also for ring and field

Author: JovanGerb

Mathlib/Analysis/Normed/Field/Basic.lean

@@ -43,6 +43,9 @@ class NormedDivisionRing (α : Type*) extends Norm α, DivisionRing α, MetricSp
   /-- The norm is multiplicative. -/
   protected norm_mul : ∀ a b, norm (a * b) = norm a * norm b
 
+-- see Note [lower instance priority]
+attribute [instance 100] NormedDivisionRing.toDivisionRing
+
 -- see Note [lower instance priority]
 /-- A normed division ring is a normed ring. -/
 instance (priority := 100) NormedDivisionRing.toNormedRing [β : NormedDivisionRing α] :
@@ -154,6 +157,9 @@ class NormedField (α : Type*) extends Norm α, Field α, MetricSpace α where
   /-- The norm is multiplicative. -/
   protected norm_mul : ∀ a b, norm (a * b) = norm a * norm b
 
+-- see Note [lower instance priority]
+attribute [instance 100] NormedField.toField
+
 /-- A nontrivially normed field is a normed field in which there is an element of norm different
 from `0` and `1`. This makes it possible to bring any element arbitrarily close to `0` by
 multiplication by the powers of any element, and thus to relate algebra and topology. -/

Mathlib/Analysis/Normed/Ring/Basic.lean

@@ -43,6 +43,9 @@ class NonUnitalSeminormedRing (α : Type*) extends Norm α, NonUnitalRing α,
   /-- The norm is submultiplicative. -/
   protected norm_mul_le : ∀ a b, norm (a * b) ≤ norm a * norm b
 
+-- see Note [lower instance priority]
+attribute [instance 100] NonUnitalSeminormedRing.toNonUnitalRing
+
 /-- A seminormed ring is a ring endowed with a seminorm which satisfies the inequality
 `‖x y‖ ≤ ‖x‖ ‖y‖`. -/
 class SeminormedRing (α : Type*) extends Norm α, Ring α, PseudoMetricSpace α where
@@ -51,6 +54,9 @@ class SeminormedRing (α : Type*) extends Norm α, Ring α, PseudoMetricSpace α
   /-- The norm is submultiplicative. -/
   norm_mul_le : ∀ a b, norm (a * b) ≤ norm a * norm b
 
+-- see Note [lower instance priority]
+attribute [instance 100] SeminormedRing.toRing
+
 -- see Note [lower instance priority]
 /-- A seminormed ring is a non-unital seminormed ring. -/
 instance (priority := 100) SeminormedRing.toNonUnitalSeminormedRing [β : SeminormedRing α] :
@@ -65,6 +71,9 @@ class NonUnitalNormedRing (α : Type*) extends Norm α, NonUnitalRing α, Metric
   /-- The norm is submultiplicative. -/
   norm_mul_le : ∀ a b, norm (a * b) ≤ norm a * norm b
 
+-- see Note [lower instance priority]
+attribute [instance 100] NonUnitalNormedRing.toNonUnitalRing
+
 -- see Note [lower instance priority]
 /-- A non-unital normed ring is a non-unital seminormed ring. -/
 instance (priority := 100) NonUnitalNormedRing.toNonUnitalSeminormedRing
@@ -78,6 +87,9 @@ class NormedRing (α : Type*) extends Norm α, Ring α, MetricSpace α where
   /-- The norm is submultiplicative. -/
   norm_mul_le : ∀ a b, norm (a * b) ≤ norm a * norm b
 
+-- see Note [lower instance priority]
+attribute [instance 100] NormedRing.toRing
+
 -- see Note [lower instance priority]
 /-- A normed ring is a seminormed ring. -/
 instance (priority := 100) NormedRing.toSeminormedRing [β : NormedRing α] : SeminormedRing α :=