# Normed fields #

In this file we define (semi)normed rings and fields. We also prove some theorems about these definitions.

class NonUnitalSeminormedRing (α : Type u_5) extends , , :
Type u_5

A non-unital seminormed ring is a not-necessarily-unital ring endowed with a seminorm which satisfies the inequality ‖x y‖ ≤ ‖x‖ ‖y‖.

• norm : α
• add_assoc : ∀ (a b c : α), a + b + c = a + (b + c)
• zero : α
• zero_add : ∀ (a : α), 0 + a = a
• add_zero : ∀ (a : α), a + 0 = a
• nsmul : αα
• nsmul_zero : ∀ (x : α), = 0
• nsmul_succ : ∀ (n : ) (x : α), AddMonoid.nsmul (n + 1) x = + x
• neg : αα
• sub : ααα
• sub_eq_add_neg : ∀ (a b : α), a - b = a + -b
• zsmul : αα
• zsmul_zero' : ∀ (a : α), = 0
• zsmul_succ' : ∀ (n : ) (a : α), SubNegMonoid.zsmul (Int.ofNat n.succ) a = + a
• zsmul_neg' : ∀ (n : ) (a : α), = -SubNegMonoid.zsmul (n.succ) a
• add_left_neg : ∀ (a : α), -a + a = 0
• add_comm : ∀ (a b : α), a + b = b + a
• mul : ααα
• left_distrib : ∀ (a b c : α), a * (b + c) = a * b + a * c
• right_distrib : ∀ (a b c : α), (a + b) * c = a * c + b * c
• zero_mul : ∀ (a : α), 0 * a = 0
• mul_zero : ∀ (a : α), a * 0 = 0
• mul_assoc : ∀ (a b c : α), a * b * c = a * (b * c)
• dist : αα
• dist_self : ∀ (x : α), dist x x = 0
• dist_comm : ∀ (x y : α), dist x y = dist y x
• dist_triangle : ∀ (x y z : α), dist x z dist x y + dist y z
• edist : ααENNReal
• edist_dist : ∀ (x y : α), = ENNReal.ofReal (dist x y)
• toUniformSpace :
• uniformity_dist : = ⨅ (ε : ), ⨅ (_ : ε > 0), Filter.principal {p : α × α | dist p.1 p.2 < ε}
• toBornology :
• cobounded_sets : .sets = {s : Set α | ∃ (C : ), xs, ys, dist x y C}
• dist_eq : ∀ (x y : α), dist x y = x - y

The distance is induced by the norm.

• norm_mul : ∀ (a b : α), a * b a * b

The norm is submultiplicative.

Instances
theorem NonUnitalSeminormedRing.dist_eq {α : Type u_5} [self : ] (x : α) (y : α) :
dist x y = x - y

The distance is induced by the norm.

theorem NonUnitalSeminormedRing.norm_mul {α : Type u_5} [self : ] (a : α) (b : α) :

The norm is submultiplicative.

class SeminormedRing (α : Type u_5) extends , , :
Type u_5

A seminormed ring is a ring endowed with a seminorm which satisfies the inequality ‖x y‖ ≤ ‖x‖ ‖y‖.

• norm : α
• add_assoc : ∀ (a b c : α), a + b + c = a + (b + c)
• zero : α
• zero_add : ∀ (a : α), 0 + a = a
• add_zero : ∀ (a : α), a + 0 = a
• nsmul : αα
• nsmul_zero : ∀ (x : α), = 0
• nsmul_succ : ∀ (n : ) (x : α), AddMonoid.nsmul (n + 1) x = + x
• add_comm : ∀ (a b : α), a + b = b + a
• mul : ααα
• left_distrib : ∀ (a b c : α), a * (b + c) = a * b + a * c
• right_distrib : ∀ (a b c : α), (a + b) * c = a * c + b * c
• zero_mul : ∀ (a : α), 0 * a = 0
• mul_zero : ∀ (a : α), a * 0 = 0
• mul_assoc : ∀ (a b c : α), a * b * c = a * (b * c)
• one : α
• one_mul : ∀ (a : α), 1 * a = a
• mul_one : ∀ (a : α), a * 1 = a
• natCast : α
• natCast_zero :
• natCast_succ : ∀ (n : ), NatCast.natCast (n + 1) =
• npow : αα
• npow_zero : ∀ (x : α), = 1
• npow_succ : ∀ (n : ) (x : α), Semiring.npow (n + 1) x = * x
• neg : αα
• sub : ααα
• sub_eq_add_neg : ∀ (a b : α), a - b = a + -b
• zsmul : αα
• zsmul_zero' : ∀ (a : α), = 0
• zsmul_succ' : ∀ (n : ) (a : α), Ring.zsmul (Int.ofNat n.succ) a = Ring.zsmul () a + a
• zsmul_neg' : ∀ (n : ) (a : α), = -Ring.zsmul (n.succ) a
• add_left_neg : ∀ (a : α), -a + a = 0
• intCast : α
• intCast_ofNat : ∀ (n : ), = n
• intCast_negSucc : ∀ (n : ), = -(n + 1)
• dist : αα
• dist_self : ∀ (x : α), dist x x = 0
• dist_comm : ∀ (x y : α), dist x y = dist y x
• dist_triangle : ∀ (x y z : α), dist x z dist x y + dist y z
• edist : ααENNReal
• edist_dist : ∀ (x y : α), = ENNReal.ofReal (dist x y)
• toUniformSpace :
• uniformity_dist : = ⨅ (ε : ), ⨅ (_ : ε > 0), Filter.principal {p : α × α | dist p.1 p.2 < ε}
• toBornology :
• cobounded_sets : .sets = {s : Set α | ∃ (C : ), xs, ys, dist x y C}
• dist_eq : ∀ (x y : α), dist x y = x - y

The distance is induced by the norm.

• norm_mul : ∀ (a b : α), a * b a * b

The norm is submultiplicative.

Instances
theorem SeminormedRing.dist_eq {α : Type u_5} [self : ] (x : α) (y : α) :
dist x y = x - y

The distance is induced by the norm.

theorem SeminormedRing.norm_mul {α : Type u_5} [self : ] (a : α) (b : α) :

The norm is submultiplicative.

@[instance 100]
instance SeminormedRing.toNonUnitalSeminormedRing {α : Type u_1} [β : ] :

A seminormed ring is a non-unital seminormed ring.

Equations
• SeminormedRing.toNonUnitalSeminormedRing =
class NonUnitalNormedRing (α : Type u_5) extends , , :
Type u_5

A non-unital normed ring is a not-necessarily-unital ring endowed with a norm which satisfies the inequality ‖x y‖ ≤ ‖x‖ ‖y‖.

• norm : α
• add_assoc : ∀ (a b c : α), a + b + c = a + (b + c)
• zero : α
• zero_add : ∀ (a : α), 0 + a = a
• add_zero : ∀ (a : α), a + 0 = a
• nsmul : αα
• nsmul_zero : ∀ (x : α), = 0
• nsmul_succ : ∀ (n : ) (x : α), AddMonoid.nsmul (n + 1) x = + x
• neg : αα
• sub : ααα
• sub_eq_add_neg : ∀ (a b : α), a - b = a + -b
• zsmul : αα
• zsmul_zero' : ∀ (a : α), = 0
• zsmul_succ' : ∀ (n : ) (a : α), SubNegMonoid.zsmul (Int.ofNat n.succ) a = + a
• zsmul_neg' : ∀ (n : ) (a : α), = -SubNegMonoid.zsmul (n.succ) a
• add_left_neg : ∀ (a : α), -a + a = 0
• add_comm : ∀ (a b : α), a + b = b + a
• mul : ααα
• left_distrib : ∀ (a b c : α), a * (b + c) = a * b + a * c
• right_distrib : ∀ (a b c : α), (a + b) * c = a * c + b * c
• zero_mul : ∀ (a : α), 0 * a = 0
• mul_zero : ∀ (a : α), a * 0 = 0
• mul_assoc : ∀ (a b c : α), a * b * c = a * (b * c)
• dist : αα
• dist_self : ∀ (x : α), dist x x = 0
• dist_comm : ∀ (x y : α), dist x y = dist y x
• dist_triangle : ∀ (x y z : α), dist x z dist x y + dist y z
• edist : ααENNReal
• edist_dist : ∀ (x y : α), = ENNReal.ofReal (dist x y)
• toUniformSpace :
• uniformity_dist : = ⨅ (ε : ), ⨅ (_ : ε > 0), Filter.principal {p : α × α | dist p.1 p.2 < ε}
• toBornology :
• cobounded_sets : .sets = {s : Set α | ∃ (C : ), xs, ys, dist x y C}
• eq_of_dist_eq_zero : ∀ {x y : α}, dist x y = 0x = y
• dist_eq : ∀ (x y : α), dist x y = x - y

The distance is induced by the norm.

• norm_mul : ∀ (a b : α), a * b a * b

The norm is submultiplicative.

Instances
theorem NonUnitalNormedRing.dist_eq {α : Type u_5} [self : ] (x : α) (y : α) :
dist x y = x - y

The distance is induced by the norm.

theorem NonUnitalNormedRing.norm_mul {α : Type u_5} [self : ] (a : α) (b : α) :

The norm is submultiplicative.

@[instance 100]

A non-unital normed ring is a non-unital seminormed ring.

Equations
• NonUnitalNormedRing.toNonUnitalSeminormedRing =
class NormedRing (α : Type u_5) extends , , :
Type u_5

A normed ring is a ring endowed with a norm which satisfies the inequality ‖x y‖ ≤ ‖x‖ ‖y‖.

• norm : α
• add_assoc : ∀ (a b c : α), a + b + c = a + (b + c)
• zero : α
• zero_add : ∀ (a : α), 0 + a = a
• add_zero : ∀ (a : α), a + 0 = a
• nsmul : αα
• nsmul_zero : ∀ (x : α), = 0
• nsmul_succ : ∀ (n : ) (x : α), AddMonoid.nsmul (n + 1) x = + x
• add_comm : ∀ (a b : α), a + b = b + a
• mul : ααα
• left_distrib : ∀ (a b c : α), a * (b + c) = a * b + a * c
• right_distrib : ∀ (a b c : α), (a + b) * c = a * c + b * c
• zero_mul : ∀ (a : α), 0 * a = 0
• mul_zero : ∀ (a : α), a * 0 = 0
• mul_assoc : ∀ (a b c : α), a * b * c = a * (b * c)
• one : α
• one_mul : ∀ (a : α), 1 * a = a
• mul_one : ∀ (a : α), a * 1 = a
• natCast : α
• natCast_zero :
• natCast_succ : ∀ (n : ), NatCast.natCast (n + 1) =
• npow : αα
• npow_zero : ∀ (x : α), = 1
• npow_succ : ∀ (n : ) (x : α), Semiring.npow (n + 1) x = * x
• neg : αα
• sub : ααα
• sub_eq_add_neg : ∀ (a b : α), a - b = a + -b
• zsmul : αα
• zsmul_zero' : ∀ (a : α), = 0
• zsmul_succ' : ∀ (n : ) (a : α), Ring.zsmul (Int.ofNat n.succ) a = Ring.zsmul () a + a
• zsmul_neg' : ∀ (n : ) (a : α), = -Ring.zsmul (n.succ) a
• add_left_neg : ∀ (a : α), -a + a = 0
• intCast : α
• intCast_ofNat : ∀ (n : ), = n
• intCast_negSucc : ∀ (n : ), = -(n + 1)
• dist : αα
• dist_self : ∀ (x : α), dist x x = 0
• dist_comm : ∀ (x y : α), dist x y = dist y x
• dist_triangle : ∀ (x y z : α), dist x z dist x y + dist y z
• edist : ααENNReal
• edist_dist : ∀ (x y : α), = ENNReal.ofReal (dist x y)
• toUniformSpace :
• uniformity_dist : = ⨅ (ε : ), ⨅ (_ : ε > 0), Filter.principal {p : α × α | dist p.1 p.2 < ε}
• toBornology :
• cobounded_sets : .sets = {s : Set α | ∃ (C : ), xs, ys, dist x y C}
• eq_of_dist_eq_zero : ∀ {x y : α}, dist x y = 0x = y
• dist_eq : ∀ (x y : α), dist x y = x - y

The distance is induced by the norm.

• norm_mul : ∀ (a b : α), a * b a * b

The norm is submultiplicative.

Instances
theorem NormedRing.dist_eq {α : Type u_5} [self : ] (x : α) (y : α) :
dist x y = x - y

The distance is induced by the norm.

theorem NormedRing.norm_mul {α : Type u_5} [self : ] (a : α) (b : α) :

The norm is submultiplicative.

class NormedDivisionRing (α : Type u_5) extends , , :
Type u_5

A normed division ring is a division ring endowed with a seminorm which satisfies the equality ‖x y‖ = ‖x‖ ‖y‖.

• norm : α
• add_assoc : ∀ (a b c : α), a + b + c = a + (b + c)
• zero : α
• zero_add : ∀ (a : α), 0 + a = a
• add_zero : ∀ (a : α), a + 0 = a
• nsmul : αα
• nsmul_zero : ∀ (x : α), = 0
• nsmul_succ : ∀ (n : ) (x : α), AddMonoid.nsmul (n + 1) x = + x
• add_comm : ∀ (a b : α), a + b = b + a
• mul : ααα
• left_distrib : ∀ (a b c : α), a * (b + c) = a * b + a * c
• right_distrib : ∀ (a b c : α), (a + b) * c = a * c + b * c
• zero_mul : ∀ (a : α), 0 * a = 0
• mul_zero : ∀ (a : α), a * 0 = 0
• mul_assoc : ∀ (a b c : α), a * b * c = a * (b * c)
• one : α
• one_mul : ∀ (a : α), 1 * a = a
• mul_one : ∀ (a : α), a * 1 = a
• natCast : α
• natCast_zero :
• natCast_succ : ∀ (n : ), NatCast.natCast (n + 1) =
• npow : αα
• npow_zero : ∀ (x : α), = 1
• npow_succ : ∀ (n : ) (x : α), Semiring.npow (n + 1) x = * x
• neg : αα
• sub : ααα
• sub_eq_add_neg : ∀ (a b : α), a - b = a + -b
• zsmul : αα
• zsmul_zero' : ∀ (a : α), = 0
• zsmul_succ' : ∀ (n : ) (a : α), Ring.zsmul (Int.ofNat n.succ) a = Ring.zsmul () a + a
• zsmul_neg' : ∀ (n : ) (a : α), = -Ring.zsmul (n.succ) a
• add_left_neg : ∀ (a : α), -a + a = 0
• intCast : α
• intCast_ofNat : ∀ (n : ), = n
• intCast_negSucc : ∀ (n : ), = -(n + 1)
• inv : αα
• div : ααα
• div_eq_mul_inv : ∀ (a b : α), a / b = a * b⁻¹
• zpow : αα
• zpow_zero' : ∀ (a : α), = 1
• zpow_succ' : ∀ (n : ) (a : α), DivisionRing.zpow (Int.ofNat n.succ) a = * a
• zpow_neg' : ∀ (n : ) (a : α), = (DivisionRing.zpow (n.succ) a)⁻¹
• exists_pair_ne : ∃ (x : α) (y : α), x y
• nnratCast : ℚ≥0α
• ratCast : α
• mul_inv_cancel : ∀ (a : α), a 0a * a⁻¹ = 1
• inv_zero : 0⁻¹ = 0
• nnratCast_def : ∀ (q : ℚ≥0), q = q.num / q.den
• nnqsmul : ℚ≥0αα
• nnqsmul_def : ∀ (q : ℚ≥0) (a : α), = q * a
• ratCast_def : ∀ (q : ), q = q.num / q.den
• qsmul : αα
• qsmul_def : ∀ (a : ) (x : α), = a * x
• dist : αα
• dist_self : ∀ (x : α), dist x x = 0
• dist_comm : ∀ (x y : α), dist x y = dist y x
• dist_triangle : ∀ (x y z : α), dist x z dist x y + dist y z
• edist : ααENNReal
• edist_dist : ∀ (x y : α), = ENNReal.ofReal (dist x y)
• toUniformSpace :
• uniformity_dist : = ⨅ (ε : ), ⨅ (_ : ε > 0), Filter.principal {p : α × α | dist p.1 p.2 < ε}
• toBornology :
• cobounded_sets : .sets = {s : Set α | ∃ (C : ), xs, ys, dist x y C}
• eq_of_dist_eq_zero : ∀ {x y : α}, dist x y = 0x = y
• dist_eq : ∀ (x y : α), dist x y = x - y

The distance is induced by the norm.

• norm_mul' : ∀ (a b : α), a * b = a * b

The norm is multiplicative.

Instances
theorem NormedDivisionRing.dist_eq {α : Type u_5} [self : ] (x : α) (y : α) :
dist x y = x - y

The distance is induced by the norm.

theorem NormedDivisionRing.norm_mul' {α : Type u_5} [self : ] (a : α) (b : α) :

The norm is multiplicative.

@[instance 100]
instance NormedDivisionRing.toNormedRing {α : Type u_1} [β : ] :

A normed division ring is a normed ring.

Equations
• NormedDivisionRing.toNormedRing =
@[instance 100]
instance NormedRing.toSeminormedRing {α : Type u_1} [β : ] :

A normed ring is a seminormed ring.

Equations
• NormedRing.toSeminormedRing =
@[instance 100]
instance NormedRing.toNonUnitalNormedRing {α : Type u_1} [β : ] :

A normed ring is a non-unital normed ring.

Equations
• NormedRing.toNonUnitalNormedRing =
class NonUnitalSeminormedCommRing (α : Type u_5) extends :
Type u_5

A non-unital seminormed commutative ring is a non-unital commutative ring endowed with a seminorm which satisfies the inequality ‖x y‖ ≤ ‖x‖ ‖y‖.

• norm : α
• add_assoc : ∀ (a b c : α), a + b + c = a + (b + c)
• zero : α
• zero_add : ∀ (a : α), 0 + a = a
• add_zero : ∀ (a : α), a + 0 = a
• nsmul : αα
• nsmul_zero : ∀ (x : α), = 0
• nsmul_succ : ∀ (n : ) (x : α), AddMonoid.nsmul (n + 1) x = + x
• neg : αα
• sub : ααα
• sub_eq_add_neg : ∀ (a b : α), a - b = a + -b
• zsmul : αα
• zsmul_zero' : ∀ (a : α), = 0
• zsmul_succ' : ∀ (n : ) (a : α), SubNegMonoid.zsmul (Int.ofNat n.succ) a = + a
• zsmul_neg' : ∀ (n : ) (a : α), = -SubNegMonoid.zsmul (n.succ) a
• add_left_neg : ∀ (a : α), -a + a = 0
• add_comm : ∀ (a b : α), a + b = b + a
• mul : ααα
• left_distrib : ∀ (a b c : α), a * (b + c) = a * b + a * c
• right_distrib : ∀ (a b c : α), (a + b) * c = a * c + b * c
• zero_mul : ∀ (a : α), 0 * a = 0
• mul_zero : ∀ (a : α), a * 0 = 0
• mul_assoc : ∀ (a b c : α), a * b * c = a * (b * c)
• dist : αα
• dist_self : ∀ (x : α), dist x x = 0
• dist_comm : ∀ (x y : α), dist x y = dist y x
• dist_triangle : ∀ (x y z : α), dist x z dist x y + dist y z
• edist : ααENNReal
• edist_dist : ∀ (x y : α), = ENNReal.ofReal (dist x y)
• toUniformSpace :
• uniformity_dist : = ⨅ (ε : ), ⨅ (_ : ε > 0), Filter.principal {p : α × α | dist p.1 p.2 < ε}
• toBornology :
• cobounded_sets : .sets = {s : Set α | ∃ (C : ), xs, ys, dist x y C}
• dist_eq : ∀ (x y : α), dist x y = x - y
• norm_mul : ∀ (a b : α), a * b a * b
• mul_comm : ∀ (x y : α), x * y = y * x

Multiplication is commutative.

Instances
theorem NonUnitalSeminormedCommRing.mul_comm {α : Type u_5} [self : ] (x : α) (y : α) :
x * y = y * x

Multiplication is commutative.

class NonUnitalNormedCommRing (α : Type u_5) extends :
Type u_5

A non-unital normed commutative ring is a non-unital commutative ring endowed with a norm which satisfies the inequality ‖x y‖ ≤ ‖x‖ ‖y‖.

• norm : α
• add_assoc : ∀ (a b c : α), a + b + c = a + (b + c)
• zero : α
• zero_add : ∀ (a : α), 0 + a = a
• add_zero : ∀ (a : α), a + 0 = a
• nsmul : αα
• nsmul_zero : ∀ (x : α), = 0
• nsmul_succ : ∀ (n : ) (x : α), AddMonoid.nsmul (n + 1) x = + x
• neg : αα
• sub : ααα
• sub_eq_add_neg : ∀ (a b : α), a - b = a + -b
• zsmul : αα
• zsmul_zero' : ∀ (a : α), = 0
• zsmul_succ' : ∀ (n : ) (a : α), SubNegMonoid.zsmul (Int.ofNat n.succ) a = + a
• zsmul_neg' : ∀ (n : ) (a : α), = -SubNegMonoid.zsmul (n.succ) a
• add_left_neg : ∀ (a : α), -a + a = 0
• add_comm : ∀ (a b : α), a + b = b + a
• mul : ααα
• left_distrib : ∀ (a b c : α), a * (b + c) = a * b + a * c
• right_distrib : ∀ (a b c : α), (a + b) * c = a * c + b * c
• zero_mul : ∀ (a : α), 0 * a = 0
• mul_zero : ∀ (a : α), a * 0 = 0
• mul_assoc : ∀ (a b c : α), a * b * c = a * (b * c)
• dist : αα
• dist_self : ∀ (x : α), dist x x = 0
• dist_comm : ∀ (x y : α), dist x y = dist y x
• dist_triangle : ∀ (x y z : α), dist x z dist x y + dist y z
• edist : ααENNReal
• edist_dist : ∀ (x y : α), = ENNReal.ofReal (dist x y)
• toUniformSpace :
• uniformity_dist : = ⨅ (ε : ), ⨅ (_ : ε > 0), Filter.principal {p : α × α | dist p.1 p.2 < ε}
• toBornology :
• cobounded_sets : .sets = {s : Set α | ∃ (C : ), xs, ys, dist x y C}
• eq_of_dist_eq_zero : ∀ {x y : α}, dist x y = 0x = y
• dist_eq : ∀ (x y : α), dist x y = x - y
• norm_mul : ∀ (a b : α), a * b a * b
• mul_comm : ∀ (x y : α), x * y = y * x

Multiplication is commutative.

Instances
theorem NonUnitalNormedCommRing.mul_comm {α : Type u_5} [self : ] (x : α) (y : α) :
x * y = y * x

Multiplication is commutative.

@[instance 100]

A non-unital normed commutative ring is a non-unital seminormed commutative ring.

Equations
• NonUnitalNormedCommRing.toNonUnitalSeminormedCommRing =
class SeminormedCommRing (α : Type u_5) extends :
Type u_5

A seminormed commutative ring is a commutative ring endowed with a seminorm which satisfies the inequality ‖x y‖ ≤ ‖x‖ ‖y‖.

• norm : α
• add_assoc : ∀ (a b c : α), a + b + c = a + (b + c)
• zero : α
• zero_add : ∀ (a : α), 0 + a = a
• add_zero : ∀ (a : α), a + 0 = a
• nsmul : αα
• nsmul_zero : ∀ (x : α), = 0
• nsmul_succ : ∀ (n : ) (x : α), AddMonoid.nsmul (n + 1) x = + x
• add_comm : ∀ (a b : α), a + b = b + a
• mul : ααα
• left_distrib : ∀ (a b c : α), a * (b + c) = a * b + a * c
• right_distrib : ∀ (a b c : α), (a + b) * c = a * c + b * c
• zero_mul : ∀ (a : α), 0 * a = 0
• mul_zero : ∀ (a : α), a * 0 = 0
• mul_assoc : ∀ (a b c : α), a * b * c = a * (b * c)
• one : α
• one_mul : ∀ (a : α), 1 * a = a
• mul_one : ∀ (a : α), a * 1 = a
• natCast : α
• natCast_zero :
• natCast_succ : ∀ (n : ), NatCast.natCast (n + 1) =
• npow : αα
• npow_zero : ∀ (x : α), = 1
• npow_succ : ∀ (n : ) (x : α), Semiring.npow (n + 1) x = * x
• neg : αα
• sub : ααα
• sub_eq_add_neg : ∀ (a b : α), a - b = a + -b
• zsmul : αα
• zsmul_zero' : ∀ (a : α), = 0
• zsmul_succ' : ∀ (n : ) (a : α), Ring.zsmul (Int.ofNat n.succ) a = Ring.zsmul () a + a
• zsmul_neg' : ∀ (n : ) (a : α), = -Ring.zsmul (n.succ) a
• add_left_neg : ∀ (a : α), -a + a = 0
• intCast : α
• intCast_ofNat : ∀ (n : ), = n
• intCast_negSucc : ∀ (n : ), = -(n + 1)
• dist : αα
• dist_self : ∀ (x : α), dist x x = 0
• dist_comm : ∀ (x y : α), dist x y = dist y x
• dist_triangle : ∀ (x y z : α), dist x z dist x y + dist y z
• edist : ααENNReal
• edist_dist : ∀ (x y : α), = ENNReal.ofReal (dist x y)
• toUniformSpace :
• uniformity_dist : = ⨅ (ε : ), ⨅ (_ : ε > 0), Filter.principal {p : α × α | dist p.1 p.2 < ε}
• toBornology :
• cobounded_sets : .sets = {s : Set α | ∃ (C : ), xs, ys, dist x y C}
• dist_eq : ∀ (x y : α), dist x y = x - y
• norm_mul : ∀ (a b : α), a * b a * b
• mul_comm : ∀ (x y : α), x * y = y * x

Multiplication is commutative.

Instances
theorem SeminormedCommRing.mul_comm {α : Type u_5} [self : ] (x : α) (y : α) :
x * y = y * x

Multiplication is commutative.

class NormedCommRing (α : Type u_5) extends :
Type u_5

A normed commutative ring is a commutative ring endowed with a norm which satisfies the inequality ‖x y‖ ≤ ‖x‖ ‖y‖.

• norm : α
• add_assoc : ∀ (a b c : α), a + b + c = a + (b + c)
• zero : α
• zero_add : ∀ (a : α), 0 + a = a
• add_zero : ∀ (a : α), a + 0 = a
• nsmul : αα
• nsmul_zero : ∀ (x : α), = 0
• nsmul_succ : ∀ (n : ) (x : α), AddMonoid.nsmul (n + 1) x = + x
• add_comm : ∀ (a b : α), a + b = b + a
• mul : ααα
• left_distrib : ∀ (a b c : α), a * (b + c) = a * b + a * c
• right_distrib : ∀ (a b c : α), (a + b) * c = a * c + b * c
• zero_mul : ∀ (a : α), 0 * a = 0
• mul_zero : ∀ (a : α), a * 0 = 0
• mul_assoc : ∀ (a b c : α), a * b * c = a * (b * c)
• one : α
• one_mul : ∀ (a : α), 1 * a = a
• mul_one : ∀ (a : α), a * 1 = a
• natCast : α
• natCast_zero :
• natCast_succ : ∀ (n : ), NatCast.natCast (n + 1) =
• npow : αα
• npow_zero : ∀ (x : α), = 1
• npow_succ : ∀ (n : ) (x : α), Semiring.npow (n + 1) x = * x
• neg : αα
• sub : ααα
• sub_eq_add_neg : ∀ (a b : α), a - b = a + -b
• zsmul : αα
• zsmul_zero' : ∀ (a : α), = 0
• zsmul_succ' : ∀ (n : ) (a : α), Ring.zsmul (Int.ofNat n.succ) a = Ring.zsmul () a + a
• zsmul_neg' : ∀ (n : ) (a : α), = -Ring.zsmul (n.succ) a
• add_left_neg : ∀ (a : α), -a + a = 0
• intCast : α
• intCast_ofNat : ∀ (n : ), = n
• intCast_negSucc : ∀ (n : ), = -(n + 1)
• dist : αα
• dist_self : ∀ (x : α), dist x x = 0
• dist_comm : ∀ (x y : α), dist x y = dist y x
• dist_triangle : ∀ (x y z : α), dist x z dist x y + dist y z
• edist : ααENNReal
• edist_dist : ∀ (x y : α), = ENNReal.ofReal (dist x y)
• toUniformSpace :
• uniformity_dist : = ⨅ (ε : ), ⨅ (_ : ε > 0), Filter.principal {p : α × α | dist p.1 p.2 < ε}
• toBornology :
• cobounded_sets : .sets = {s : Set α | ∃ (C : ), xs, ys, dist x y C}
• eq_of_dist_eq_zero : ∀ {x y : α}, dist x y = 0x = y
• dist_eq : ∀ (x y : α), dist x y = x - y
• norm_mul : ∀ (a b : α), a * b a * b
• mul_comm : ∀ (x y : α), x * y = y * x

Multiplication is commutative.

Instances
theorem NormedCommRing.mul_comm {α : Type u_5} [self : ] (x : α) (y : α) :
x * y = y * x

Multiplication is commutative.

@[instance 100]

A seminormed commutative ring is a non-unital seminormed commutative ring.

Equations
• SeminormedCommRing.toNonUnitalSeminormedCommRing =
@[instance 100]
instance NormedCommRing.toNonUnitalNormedCommRing {α : Type u_1} [β : ] :

A normed commutative ring is a non-unital normed commutative ring.

Equations
• NormedCommRing.toNonUnitalNormedCommRing =
@[instance 100]
instance NormedCommRing.toSeminormedCommRing {α : Type u_1} [β : ] :

A normed commutative ring is a seminormed commutative ring.

Equations
• NormedCommRing.toSeminormedCommRing =
class NormOneClass (α : Type u_5) [Norm α] [One α] :

A mixin class with the axiom ‖1‖ = 1. Many NormedRings and all NormedFields satisfy this axiom.

• norm_one : 1 = 1

The norm of the multiplicative identity is 1.

Instances
@[simp]
theorem NormOneClass.norm_one {α : Type u_5} [Norm α] [One α] [self : ] :

The norm of the multiplicative identity is 1.

@[simp]
theorem nnnorm_one {α : Type u_1} [One α] [] :
theorem NormOneClass.nontrivial (α : Type u_5) [One α] [] :
@[instance 100]
Equations
• NonUnitalSeminormedCommRing.toNonUnitalCommRing =
@[instance 100]
instance SeminormedCommRing.toCommRing {α : Type u_1} [β : ] :
Equations
• SeminormedCommRing.toCommRing =
@[instance 100]
instance NonUnitalNormedRing.toNormedAddCommGroup {α : Type u_1} [β : ] :
Equations
@[instance 100]
Equations
• NonUnitalSeminormedRing.toSeminormedAddCommGroup = let __src := inst;
instance ULift.normOneClass {α : Type u_1} [One α] [] :
Equations
• =
instance Prod.normOneClass {α : Type u_1} {β : Type u_2} [One α] [] [One β] [] :
Equations
• =
instance Pi.normOneClass {ι : Type u_5} {α : ιType u_6} [] [] [(i : ι) → ] [(i : ι) → One (α i)] [∀ (i : ι), NormOneClass (α i)] :
NormOneClass ((i : ι) → α i)
Equations
• =
instance MulOpposite.normOneClass {α : Type u_1} [One α] [] :
Equations
• =
theorem norm_mul_le {α : Type u_1} (a : α) (b : α) :
theorem nnnorm_mul_le {α : Type u_1} (a : α) (b : α) :
theorem one_le_norm_one (β : Type u_5) [] [] :
theorem one_le_nnnorm_one (β : Type u_5) [] [] :
theorem Filter.Tendsto.zero_mul_isBoundedUnder_le {α : Type u_1} {ι : Type u_4} {f : ια} {g : ια} {l : } (hf : Filter.Tendsto f l (nhds 0)) (hg : Filter.IsBoundedUnder (fun (x x_1 : ) => x x_1) l ((fun (x : α) => x) g)) :
Filter.Tendsto (fun (x : ι) => f x * g x) l (nhds 0)
theorem Filter.isBoundedUnder_le_mul_tendsto_zero {α : Type u_1} {ι : Type u_4} {f : ια} {g : ια} {l : } (hf : Filter.IsBoundedUnder (fun (x x_1 : ) => x x_1) l (norm f)) (hg : Filter.Tendsto g l (nhds 0)) :
Filter.Tendsto (fun (x : ι) => f x * g x) l (nhds 0)
theorem mulLeft_bound {α : Type u_1} (x : α) (y : α) :

In a seminormed ring, the left-multiplication AddMonoidHom is bounded.

theorem mulRight_bound {α : Type u_1} (x : α) (y : α) :

In a seminormed ring, the right-multiplication AddMonoidHom is bounded.

instance NonUnitalSubalgebra.nonUnitalSeminormedRing {𝕜 : Type u_5} [] {E : Type u_6} [Module 𝕜 E] (s : ) :

A non-unital subalgebra of a non-unital seminormed ring is also a non-unital seminormed ring, with the restriction of the norm.

Equations
• s.nonUnitalSeminormedRing = let __src := s.toSubmodule.seminormedAddCommGroup; let __src_1 := s.toNonUnitalRing;
instance NonUnitalSubalgebra.nonUnitalNormedRing {𝕜 : Type u_5} [] {E : Type u_6} [Module 𝕜 E] (s : ) :

A non-unital subalgebra of a non-unital normed ring is also a non-unital normed ring, with the restriction of the norm.

Equations
• s.nonUnitalNormedRing = let __src := s.nonUnitalSeminormedRing;
instance ULift.nonUnitalSeminormedRing {α : Type u_1} :
Equations
• ULift.nonUnitalSeminormedRing = let __src := ULift.seminormedAddCommGroup; let __src_1 := ULift.nonUnitalRing;
instance Prod.nonUnitalSeminormedRing {α : Type u_1} {β : Type u_2} :

Non-unital seminormed ring structure on the product of two non-unital seminormed rings, using the sup norm.

Equations
• Prod.nonUnitalSeminormedRing = let __src := Prod.seminormedAddCommGroup; let __src_1 := Prod.instNonUnitalRing;
instance Pi.nonUnitalSeminormedRing {ι : Type u_4} {π : ιType u_5} [] [(i : ι) → ] :
NonUnitalSeminormedRing ((i : ι) → π i)

Non-unital seminormed ring structure on the product of finitely many non-unital seminormed rings, using the sup norm.

Equations
• Pi.nonUnitalSeminormedRing = let __src := Pi.seminormedAddCommGroup; let __src_1 := Pi.nonUnitalRing;
Equations
instance Subalgebra.seminormedRing {𝕜 : Type u_5} [] {E : Type u_6} [] [Algebra 𝕜 E] (s : ) :

A subalgebra of a seminormed ring is also a seminormed ring, with the restriction of the norm.

Equations
• s.seminormedRing = let __src := (Subalgebra.toSubmodule s).seminormedAddCommGroup; let __src_1 := s.toRing;
instance Subalgebra.normedRing {𝕜 : Type u_5} [] {E : Type u_6} [] [Algebra 𝕜 E] (s : ) :

A subalgebra of a normed ring is also a normed ring, with the restriction of the norm.

Equations
• s.normedRing = let __src := s.seminormedRing;
theorem Nat.norm_cast_le {α : Type u_1} [] (n : ) :
n n * 1
theorem List.norm_prod_le' {α : Type u_1} [] {l : List α} :
l []l.prod (List.map norm l).prod
theorem List.nnnorm_prod_le' {α : Type u_1} [] {l : List α} (hl : l []) :
l.prod‖₊ (List.map nnnorm l).prod
theorem List.norm_prod_le {α : Type u_1} [] [] (l : List α) :
l.prod (List.map norm l).prod
theorem List.nnnorm_prod_le {α : Type u_1} [] [] (l : List α) :
l.prod‖₊ (List.map nnnorm l).prod
theorem Finset.norm_prod_le' {ι : Type u_4} {α : Type u_5} [] (s : ) (hs : s.Nonempty) (f : ια) :
is, f i is, f i
theorem Finset.nnnorm_prod_le' {ι : Type u_4} {α : Type u_5} [] (s : ) (hs : s.Nonempty) (f : ια) :
is, f i‖₊ is, f i‖₊
theorem Finset.norm_prod_le {ι : Type u_4} {α : Type u_5} [] [] (s : ) (f : ια) :
is, f i is, f i
theorem Finset.nnnorm_prod_le {ι : Type u_4} {α : Type u_5} [] [] (s : ) (f : ια) :
is, f i‖₊ is, f i‖₊
theorem nnnorm_pow_le' {α : Type u_1} [] (a : α) {n : } :
0 < na ^ n‖₊ a‖₊ ^ n

If α is a seminormed ring, then ‖a ^ n‖₊ ≤ ‖a‖₊ ^ n for n > 0. See also nnnorm_pow_le.

theorem nnnorm_pow_le {α : Type u_1} [] [] (a : α) (n : ) :

If α is a seminormed ring with ‖1‖₊ = 1, then ‖a ^ n‖₊ ≤ ‖a‖₊ ^ n. See also nnnorm_pow_le'.

theorem norm_pow_le' {α : Type u_1} [] (a : α) {n : } (h : 0 < n) :

If α is a seminormed ring, then ‖a ^ n‖ ≤ ‖a‖ ^ n for n > 0. See also norm_pow_le.

theorem norm_pow_le {α : Type u_1} [] [] (a : α) (n : ) :

If α is a seminormed ring with ‖1‖ = 1, then ‖a ^ n‖ ≤ ‖a‖ ^ n. See also norm_pow_le'.

theorem eventually_norm_pow_le {α : Type u_1} [] (a : α) :
∀ᶠ (n : ) in Filter.atTop, a ^ n a ^ n
instance ULift.seminormedRing {α : Type u_1} [] :
Equations
• ULift.seminormedRing = let __src := ULift.nonUnitalSeminormedRing; let __src_1 := ULift.ring;
instance Prod.seminormedRing {α : Type u_1} {β : Type u_2} [] [] :

Seminormed ring structure on the product of two seminormed rings, using the sup norm.

Equations
• Prod.seminormedRing = let __src := Prod.nonUnitalSeminormedRing; let __src_1 := Prod.instRing;
instance Pi.seminormedRing {ι : Type u_4} {π : ιType u_5} [] [(i : ι) → SeminormedRing (π i)] :
SeminormedRing ((i : ι) → π i)

Seminormed ring structure on the product of finitely many seminormed rings, using the sup norm.

Equations
• Pi.seminormedRing = let __src := Pi.nonUnitalSeminormedRing; let __src_1 := Pi.ring;
instance MulOpposite.instSeminormedRing {α : Type u_1} [] :
Equations
Equations
• ULift.nonUnitalNormedRing = let __src := ULift.nonUnitalSeminormedRing; let __src_1 := ULift.normedAddCommGroup;
instance Prod.nonUnitalNormedRing {α : Type u_1} {β : Type u_2} :

Non-unital normed ring structure on the product of two non-unital normed rings, using the sup norm.

Equations
• Prod.nonUnitalNormedRing = let __src := Prod.nonUnitalSeminormedRing; let __src_1 := Prod.normedAddCommGroup;
instance Pi.nonUnitalNormedRing {ι : Type u_4} {π : ιType u_5} [] [(i : ι) → NonUnitalNormedRing (π i)] :
NonUnitalNormedRing ((i : ι) → π i)

Normed ring structure on the product of finitely many non-unital normed rings, using the sup norm.

Equations
• Pi.nonUnitalNormedRing = let __src := Pi.nonUnitalSeminormedRing; let __src_1 := Pi.normedAddCommGroup;
Equations
• One or more equations did not get rendered due to their size.
theorem Units.norm_pos {α : Type u_1} [] [] (x : αˣ) :
0 < x
theorem Units.nnnorm_pos {α : Type u_1} [] [] (x : αˣ) :
0 < x‖₊
instance ULift.normedRing {α : Type u_1} [] :
Equations
• ULift.normedRing = let __src := ULift.seminormedRing; let __src_1 := ULift.normedAddCommGroup;
instance Prod.normedRing {α : Type u_1} {β : Type u_2} [] [] :
NormedRing (α × β)

Normed ring structure on the product of two normed rings, using the sup norm.

Equations
• Prod.normedRing = let __src := Prod.nonUnitalNormedRing; let __src_1 := Prod.instRing;
instance Pi.normedRing {ι : Type u_4} {π : ιType u_5} [] [(i : ι) → NormedRing (π i)] :
NormedRing ((i : ι) → π i)

Normed ring structure on the product of finitely many normed rings, using the sup norm.

Equations
• Pi.normedRing = let __src := Pi.seminormedRing; let __src_1 := Pi.normedAddCommGroup;
instance MulOpposite.instNormedRing {α : Type u_1} [] :
Equations
Equations
• ULift.nonUnitalSeminormedCommRing = let __src := ULift.nonUnitalSeminormedRing; let __src_1 := ULift.nonUnitalCommRing;
instance Prod.nonUnitalSeminormedCommRing {α : Type u_1} {β : Type u_2} :

Non-unital seminormed commutative ring structure on the product of two non-unital seminormed commutative rings, using the sup norm.

Equations
• Prod.nonUnitalSeminormedCommRing = let __src := Prod.nonUnitalSeminormedRing; let __src_1 := Prod.instNonUnitalCommRing;
instance Pi.nonUnitalSeminormedCommRing {ι : Type u_4} {π : ιType u_5} [] [(i : ι) → ] :
NonUnitalSeminormedCommRing ((i : ι) → π i)

Non-unital seminormed commutative ring structure on the product of finitely many non-unital seminormed commutative rings, using the sup norm.

Equations
• Pi.nonUnitalSeminormedCommRing = let __src := Pi.nonUnitalSeminormedRing; let __src_1 := Pi.nonUnitalCommRing;
Equations
instance NonUnitalSubalgebra.nonUnitalSeminormedCommRing {𝕜 : Type u_5} [] {E : Type u_6} [Module 𝕜 E] (s : ) :

A non-unital subalgebra of a non-unital seminormed commutative ring is also a non-unital seminormed commutative ring, with the restriction of the norm.

Equations
• s.nonUnitalSeminormedCommRing = let __src := s.nonUnitalSeminormedRing; let __src_1 := s.toNonUnitalCommRing;
instance NonUnitalSubalgebra.nonUnitalNormedCommRing {𝕜 : Type u_5} [] {E : Type u_6} [Module 𝕜 E] (s : ) :

A non-unital subalgebra of a non-unital normed commutative ring is also a non-unital normed commutative ring, with the restriction of the norm.

Equations
• s.nonUnitalNormedCommRing = let __src := s.nonUnitalSeminormedCommRing; let __src_1 := s.nonUnitalNormedRing;
instance ULift.nonUnitalNormedCommRing {α : Type u_1} :
Equations
• ULift.nonUnitalNormedCommRing = let __src := ULift.nonUnitalSeminormedCommRing; let __src_1 := ULift.normedAddCommGroup;
instance Prod.nonUnitalNormedCommRing {α : Type u_1} {β : Type u_2} :

Non-unital normed commutative ring structure on the product of two non-unital normed commutative rings, using the sup norm.

Equations
• Prod.nonUnitalNormedCommRing = let __src := Prod.nonUnitalSeminormedCommRing; let __src_1 := Prod.normedAddCommGroup;
instance Pi.nonUnitalNormedCommRing {ι : Type u_4} {π : ιType u_5} [] [(i : ι) → ] :
NonUnitalNormedCommRing ((i : ι) → π i)

Normed commutative ring structure on the product of finitely many non-unital normed commutative rings, using the sup norm.

Equations
• Pi.nonUnitalNormedCommRing = let __src := Pi.nonUnitalSeminormedCommRing; let __src_1 := Pi.normedAddCommGroup;
Equations
Equations
• ULift.seminormedCommRing = let __src := ULift.nonUnitalSeminormedRing; let __src_1 := ULift.commRing;
instance Prod.seminormedCommRing {α : Type u_1} {β : Type u_2} :

Seminormed commutative ring structure on the product of two seminormed commutative rings, using the sup norm.

Equations
• Prod.seminormedCommRing = let __src := Prod.nonUnitalSeminormedCommRing; let __src_1 := Prod.instCommRing;
instance Pi.seminormedCommRing {ι : Type u_4} {π : ιType u_5} [] [(i : ι) → SeminormedCommRing (π i)] :
SeminormedCommRing ((i : ι) → π i)

Seminormed commutative ring structure on the product of finitely many seminormed commutative rings, using the sup norm.

Equations
• Pi.seminormedCommRing = let __src := Pi.nonUnitalSeminormedCommRing; let __src_1 := Pi.ring;
Equations
instance Subalgebra.seminormedCommRing {𝕜 : Type u_5} [] {E : Type u_6} [Algebra 𝕜 E] (s : ) :

A subalgebra of a seminormed commutative ring is also a seminormed commutative ring, with the restriction of the norm.

Equations
• s.seminormedCommRing = let __src := s.seminormedRing; let __src_1 := s.toCommRing;
instance Subalgebra.normedCommRing {𝕜 : Type u_5} [] {E : Type u_6} [] [Algebra 𝕜 E] (s : ) :

A subalgebra of a normed commutative ring is also a normed commutative ring, with the restriction of the norm.

Equations
• s.normedCommRing = let __src := s.seminormedCommRing; let __src_1 := s.normedRing;
instance ULift.normedCommRing {α : Type u_1} [] :
Equations
• ULift.normedCommRing = let __src := ULift.normedRing; let __src_1 := ULift.seminormedCommRing;
instance Prod.normedCommRing {α : Type u_1} {β : Type u_2} [] [] :

Normed commutative ring structure on the product of two normed commutative rings, using the sup norm.

Equations
• Prod.normedCommRing = let __src := Prod.nonUnitalNormedRing; let __src_1 := Prod.instCommRing;
instance Pi.normedCommutativeRing {ι : Type u_4} {π : ιType u_5} [] [(i : ι) → NormedCommRing (π i)] :
NormedCommRing ((i : ι) → π i)

Normed commutative ring structure on the product of finitely many normed commutative rings, using the sup norm.

Equations
• Pi.normedCommutativeRing = let __src := Pi.seminormedCommRing; let __src_1 := Pi.normedAddCommGroup;
instance MulOpposite.instNormedCommRing {α : Type u_1} [] :
Equations
@[instance 100]
instance semi_normed_ring_top_monoid {α : Type u_1} :
Equations
• =
@[instance 100]
instance semi_normed_top_ring {α : Type u_1} :

A seminormed ring is a topological ring.

Equations
• =
@[simp]
theorem norm_mul {α : Type u_1} (a : α) (b : α) :
@[instance 900]
Equations
• =
instance isAbsoluteValue_norm {α : Type u_1} :
Equations
• =
@[simp]
theorem nnnorm_mul {α : Type u_1} (a : α) (b : α) :
@[simp]
theorem normHom_apply {α : Type u_1} :
∀ (x : α), normHom x = x
def normHom {α : Type u_1} :

norm as a MonoidWithZeroHom.

Equations
• normHom = { toFun := fun (x : α) => x, map_zero' := , map_one' := , map_mul' := }
Instances For
@[simp]
theorem nnnormHom_apply {α : Type u_1} :
∀ (x : α), nnnormHom x = x‖₊
def nnnormHom {α : Type u_1} :

nnnorm as a MonoidWithZeroHom.

Equations
• nnnormHom = { toFun := fun (x : α) => x‖₊, map_zero' := , map_one' := , map_mul' := }
Instances For
@[simp]
theorem norm_pow {α : Type u_1} (a : α) (n : ) :
a ^ n = a ^ n
@[simp]
theorem nnnorm_pow {α : Type u_1} (a : α) (n : ) :
theorem List.norm_prod {α : Type u_1} (l : List α) :
l.prod = (List.map norm l).prod
theorem List.nnnorm_prod {α : Type u_1} (l : List α) :
l.prod‖₊ = (List.map nnnorm l).prod
@[simp]
theorem norm_div {α : Type u_1} (a : α) (b : α) :
@[simp]
theorem nnnorm_div {α : Type u_1} (a : α) (b : α) :
@[simp]
theorem norm_inv {α : Type u_1} (a : α) :
@[simp]
theorem nnnorm_inv {α : Type u_1} (a : α) :
@[simp]
theorem norm_zpow {α : Type u_1} (a : α) (n : ) :
a ^ n = a ^ n
@[simp]
theorem nnnorm_zpow {α : Type u_1} (a : α) (n : ) :
theorem dist_inv_inv₀ {α : Type u_1} {z : α} {w : α} (hz : z 0) (hw : w 0) :
theorem nndist_inv_inv₀ {α : Type u_1} {z : α} {w : α} (hz : z 0) (hw : w 0) :
theorem antilipschitzWith_mul_left {α : Type u_1} {a : α} (ha : a 0) :
AntilipschitzWith fun (x : α) => a * x
theorem antilipschitzWith_mul_right {α : Type u_1} {a : α} (ha : a 0) :
AntilipschitzWith fun (x : α) => x * a
@[simp]
theorem DilationEquiv.mulLeft_symm_apply {α : Type u_1} (a : α) (ha : a 0) (x : α) :
().symm x = a⁻¹ * x
@[simp]
theorem DilationEquiv.mulLeft_apply {α : Type u_1} (a : α) (ha : a 0) (x : α) :
() x = a * x
def DilationEquiv.mulLeft {α : Type u_1} (a : α) (ha : a 0) :
α ≃ᵈ α

Multiplication by a nonzero element a on the left as a DilationEquiv of a normed division ring.

Equations
• = { toEquiv := , edist_eq' := }
Instances For
@[simp]
theorem DilationEquiv.mulRight_symm_apply {α : Type u_1} (a : α) (ha : a 0) (x : α) :
().symm x = x * a⁻¹
@[simp]
theorem DilationEquiv.mulRight_apply {α : Type u_1} (a : α) (ha : a 0) (x : α) :
() x = x * a
def DilationEquiv.mulRight {α : Type u_1} (a : α) (ha : a 0) :
α ≃ᵈ α

Multiplication by a nonzero element a on the right as a DilationEquiv of a normed division ring.

Equations
• = { toEquiv := , edist_eq' := }
Instances For
@[simp]
theorem Filter.comap_mul_left_cobounded {α : Type u_1} {a : α} (ha : a 0) :
Filter.comap (fun (x : α) => a * x) =
@[simp]
theorem Filter.map_mul_left_cobounded {α : Type u_1} {a : α} (ha : a 0) :
Filter.map (fun (x : α) => a * x) =
@[simp]
theorem Filter.comap_mul_right_cobounded {α : Type u_1} {a : α} (ha : a 0) :
Filter.comap (fun (x : α) => x * a) =
@[simp]
theorem Filter.map_mul_right_cobounded {α : Type u_1} {a : α} (ha : a 0) :
Filter.map (fun (x : α) => x * a) =
theorem Filter.tendsto_mul_left_cobounded {α : Type u_1} {a : α} (ha : a 0) :
Filter.Tendsto (fun (x : α) => a * x)

Multiplication on the left by a nonzero element of a normed division ring tends to infinity at infinity.

theorem Filter.tendsto_mul_right_cobounded {α : Type u_1} {a : α} (ha : a 0) :
Filter.Tendsto (fun (x : α) => x * a)

Multiplication on the right by a nonzero element of a normed division ring tends to infinity at infinity.

@[simp]
theorem Filter.inv_cobounded₀ {α : Type u_1} :
@[simp]
@[instance 100]
Equations
• =
@[instance 100]

A normed division ring is a topological division ring.

Equations
• =
theorem IsOfFinOrder.norm_eq_one {α : Type u_1} {a : α} (ha : ) :
class NormedField (α : Type u_5) extends , , :
Type u_5

A normed field is a field with a norm satisfying ‖x y‖ = ‖x‖ ‖y‖.

• norm : α
• add_assoc : ∀ (a b c : α), a + b + c = a + (b + c)
• zero : α
• zero_add : ∀ (a : α), 0 + a = a
• add_zero : ∀ (a : α), a + 0 = a
• nsmul : αα
• nsmul_zero : ∀ (x : α), = 0
• nsmul_succ : ∀ (n : ) (x : α), AddMonoid.nsmul (n + 1) x = + x
• add_comm : ∀ (a b : α), a + b = b + a
• mul : ααα
• left_distrib : ∀ (a b c : α), a * (b + c) = a * b + a * c
• right_distrib : ∀ (a b c : α), (a + b) * c = a * c + b * c
• zero_mul : ∀ (a : α), 0 * a = 0
• mul_zero : ∀ (a : α), a * 0 = 0
• mul_assoc : ∀ (a b c : α), a * b * c = a * (b * c)
• one : α
• one_mul : ∀ (a : α), 1 * a = a
• mul_one : ∀ (a : α), a * 1 = a
• natCast : α
• natCast_zero :
• natCast_succ : ∀ (n : ), NatCast.natCast (n + 1) =
• npow : αα
• npow_zero : ∀ (x : α), = 1
• npow_succ : ∀ (n : ) (x : α), Semiring.npow (n + 1) x = * x
• neg : αα
• sub : ααα
• sub_eq_add_neg : ∀ (a b : α), a - b = a + -b
• zsmul : αα
• zsmul_zero' : ∀ (a : α), = 0
• zsmul_succ' : ∀ (n : ) (a : α), Ring.zsmul (Int.ofNat n.succ) a = Ring.zsmul () a + a
• zsmul_neg' : ∀ (n : ) (a : α), = -Ring.zsmul (n.succ) a
• add_left_neg : ∀ (a : α), -a + a = 0
• intCast : α
• intCast_ofNat : ∀ (n : ), = n
• intCast_negSucc : ∀ (n : ), = -(n + 1)
• mul_comm : ∀ (a b : α), a * b = b * a
• inv : αα
• div : ααα
• div_eq_mul_inv : ∀ (a b : α), a / b = a * b⁻¹
• zpow : αα
• zpow_zero' : ∀ (a : α), = 1
• zpow_succ' : ∀ (n : ) (a : α), Field.zpow (Int.ofNat n.succ) a = Field.zpow () a * a
• zpow_neg' : ∀ (n : ) (a : α), = (Field.zpow (n.succ) a)⁻¹
• exists_pair_ne : ∃ (x : α) (y : α), x y
• nnratCast : ℚ≥0α
• ratCast : α
• mul_inv_cancel : ∀ (a : α), a 0a * a⁻¹ = 1
• inv_zero : 0⁻¹ = 0
• nnratCast_def : ∀ (q : ℚ≥0), q = q.num / q.den
• nnqsmul : ℚ≥0αα
• nnqsmul_def : ∀ (q : ℚ≥0) (a : α), = q * a
• ratCast_def : ∀ (q : ), q = q.num / q.den
• qsmul : αα
• qsmul_def : ∀ (a : ) (x : α), = a * x
• dist : αα
• dist_self : ∀ (x : α), dist x x = 0
• dist_comm : ∀ (x y : α), dist x y = dist y x
• dist_triangle : ∀ (x y z : α), dist x z dist x y + dist y z
• edist : ααENNReal
• edist_dist : ∀ (x y : α), = ENNReal.ofReal (dist x y)
• toUniformSpace :
• uniformity_dist : = ⨅ (ε : ), ⨅ (_ : ε > 0), Filter.principal {p : α × α | dist p.1 p.2 < ε}
• toBornology :
• cobounded_sets : .sets = {s : Set α | ∃ (C : ), xs, ys, dist x y C}
• eq_of_dist_eq_zero : ∀ {x y : α}, dist x y = 0x = y
• dist_eq : ∀ (x y : α), dist x y = x - y

The distance is induced by the norm.

• norm_mul' : ∀ (a b : α), a * b = a * b

The norm is multiplicative.

Instances
theorem NormedField.dist_eq {α : Type u_5} [self : ] (x : α) (y : α) :
dist x y = x - y

The distance is induced by the norm.

theorem NormedField.norm_mul' {α : Type u_5} [self : ] (a : α) (b : α) :

The norm is multiplicative.

class NontriviallyNormedField (α : Type u_5) extends :
Type u_5

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.

• norm : α
• add_assoc : ∀ (a b c : α), a + b + c = a + (b + c)
• zero : α
• zero_add : ∀ (a : α), 0 + a = a
• add_zero : ∀ (a : α), a + 0 = a
• nsmul : αα
• nsmul_zero : ∀ (x : α), = 0
• nsmul_succ : ∀ (n : ) (x : α), AddMonoid.nsmul (n + 1) x = + x
• add_comm : ∀ (a b : α), a + b = b + a
• mul : ααα
• left_distrib : ∀ (a b c : α), a * (b + c) = a * b + a * c
• right_distrib : ∀ (a b c : α), (a + b) * c = a * c + b * c
• zero_mul : ∀ (a : α), 0 * a = 0
• mul_zero : ∀ (a : α), a * 0 = 0
• mul_assoc : ∀ (a b c : α), a * b * c = a * (b * c)
• one : α
• one_mul : ∀ (a : α), 1 * a = a
• mul_one : ∀ (a : α), a * 1 = a
• natCast : α
• natCast_zero :
• natCast_succ : ∀ (n : ), NatCast.natCast (n + 1) =
• npow : αα
• npow_zero : ∀ (x : α), = 1
• npow_succ : ∀ (n : ) (x : α), Semiring.npow (n + 1) x = * x
• neg : αα
• sub : ααα
• sub_eq_add_neg : ∀ (a b : α), a - b = a + -b
• zsmul : αα
• zsmul_zero' : ∀ (a : α), = 0
• zsmul_succ' : ∀ (n : ) (a : α), Ring.zsmul (Int.ofNat n.succ) a = Ring.zsmul () a + a
• zsmul_neg' : ∀ (n : ) (a : α), = -Ring.zsmul (n.succ) a
• add_left_neg : ∀ (a : α), -a + a = 0
• intCast : α
• intCast_ofNat : ∀ (n : ), = n
• intCast_negSucc : ∀ (n : ), = -(n + 1)
• mul_comm : ∀ (a b : α), a * b = b * a
• inv : αα
• div : ααα
• div_eq_mul_inv : ∀ (a b : α), a / b = a * b⁻¹
• zpow : αα
• zpow_zero' : ∀ (a : α), = 1
• zpow_succ' : ∀ (n : ) (a : α), Field.zpow (Int.ofNat n.succ) a = Field.zpow () a * a
• zpow_neg' : ∀ (n : ) (a : α), = (Field.zpow (n.succ) a)⁻¹
• exists_pair_ne : ∃ (x : α) (y : α), x y
• nnratCast : ℚ≥0α
• ratCast : α
• mul_inv_cancel : ∀ (a : α), a 0a * a⁻¹ = 1
• inv_zero : 0⁻¹ = 0
• nnratCast_def : ∀ (q : ℚ≥0), q = q.num / q.den
• nnqsmul : ℚ≥0αα
• nnqsmul_def : ∀ (q : ℚ≥0) (a : α), = q * a
• ratCast_def : ∀ (q : ), q = q.num / q.den
• qsmul : αα
• qsmul_def : ∀ (a : ) (x : α), = a * x
• dist : αα
• dist_self : ∀ (x : α), dist x x = 0
• dist_comm : ∀ (x y : α), dist x y = dist y x
• dist_triangle : ∀ (x y z : α), dist x z dist x y + dist y z
• edist : ααENNReal
• edist_dist : ∀ (x y : α), = ENNReal.ofReal (dist x y)
• toUniformSpace :
• uniformity_dist : = ⨅ (ε : ), ⨅ (_ : ε > 0), Filter.principal {p : α × α | dist p.1 p.2 < ε}
• toBornology :
• cobounded_sets : .sets = {s : Set α | ∃ (C : ), xs, ys, dist x y C}
• eq_of_dist_eq_zero : ∀ {x y : α}, dist x y = 0x = y
• dist_eq : ∀ (x y : α), dist x y = x - y
• norm_mul' : ∀ (a b : α), a * b = a * b
• non_trivial : ∃ (x : α), 1 < x

The norm attains a value exceeding 1.

Instances
theorem NontriviallyNormedField.non_trivial {α : Type u_5} [self : ] :
∃ (x : α), 1 < x

The norm attains a value exceeding 1.

class DenselyNormedField (α : Type u_5) extends :
Type u_5

A densely normed field is a normed field for which the image of the norm is dense in ℝ≥0, which means it is also nontrivially normed. However, not all nontrivally normed fields are densely normed; in particular, the Padics exhibit this fact.

• norm : α
• add_assoc : ∀ (a b c : α), a + b + c = a + (b + c)
• zero : α
• zero_add : ∀ (a : α), 0 + a = a
• add_zero : ∀ (a : α), a + 0 = a
• nsmul : αα
• nsmul_zero : ∀ (x : α), = 0
• nsmul_succ : ∀ (n : ) (x : α), AddMonoid.nsmul (n + 1) x = + x
• add_comm : ∀ (a b : α), a + b = b + a
• mul : ααα
• left_distrib : ∀ (a b c : α), a * (b + c) = a * b + a * c
• right_distrib : ∀ (a b c : α), (a + b) * c = a * c + b * c
• zero_mul : ∀ (a : α), 0 * a = 0
• mul_zero : ∀ (a : α), a * 0 = 0
• mul_assoc : ∀ (a b c : α), a * b * c = a * (b * c)
• one : α
• one_mul : ∀ (a : α), 1 * a = a
• mul_one : ∀ (a : α), a * 1 = a
• natCast : α
• natCast_zero :
• natCast_succ : ∀ (n : ), NatCast.natCast (n + 1) =
• npow : αα
• npow_zero : ∀ (x : α), = 1
• npow_succ : ∀ (n : ) (x : α), Semiring.npow (n + 1) x = * x
• neg : αα
• sub : ααα
• sub_eq_add_neg : ∀ (a b : α), a - b = a + -b
• zsmul : αα
• zsmul_zero' : ∀ (a : α), = 0
• zsmul_succ' : ∀ (n : ) (a : α), Ring.zsmul (Int.ofNat n.succ) a = Ring.zsmul () a + a
• zsmul_neg' : ∀ (n : ) (a : α), = -Ring.zsmul (n.succ) a
• add_left_neg : ∀ (a : α), -a + a = 0
• intCast : α
• intCast_ofNat : ∀ (n : ), = n
• intCast_negSucc : ∀ (n : ), = -(n + 1)
• mul_comm : ∀ (a b : α), a * b = b * a
• inv : αα
• div : ααα
• div_eq_mul_inv : ∀ (a b : α), a / b = a * b⁻¹
• zpow : αα
• zpow_zero' : ∀ (a : α), = 1
• zpow_succ' : ∀ (n : ) (a : α), Field.zpow (Int.ofNat n.succ) a = Field.zpow () a * a
• zpow_neg' : ∀ (n : ) (a : α), = (Field.zpow (n.succ) a)⁻¹
• exists_pair_ne : ∃ (x : α) (y : α), x y
• nnratCast : ℚ≥0α
• ratCast : α
• mul_inv_cancel : ∀ (a : α), a 0a * a⁻¹ = 1
• inv_zero : 0⁻¹ = 0
• nnratCast_def : ∀ (q : ℚ≥0), q = q.num / q.den
• nnqsmul : ℚ≥0αα
• nnqsmul_def : ∀ (q : ℚ≥0) (a : α), = q * a
• ratCast_def : ∀ (q : ), q = q.num / q.den
• qsmul : αα
• qsmul_def : ∀ (a : ) (x : α), = a * x
• dist : αα
• dist_self : ∀ (x : α), dist x x = 0
• dist_comm : ∀ (x y : α), dist x y = dist y x
• dist_triangle : ∀ (x y z : α), dist x z dist x y + dist y z
• edist : ααENNReal
• edist_dist : ∀ (x y : α), = ENNReal.ofReal (dist x y)
• toUniformSpace :
• uniformity_dist : = ⨅ (ε : ), ⨅ (_ : ε > 0), Filter.principal {p : α × α | dist p.1 p.2 < ε}
• toBornology :
• cobounded_sets : .sets = {s : Set α | ∃ (C : ), xs, ys, dist x y C}
• eq_of_dist_eq_zero : ∀ {x y : α}, dist x y = 0x = y
• dist_eq : ∀ (x y : α), dist x y = x - y
• norm_mul' : ∀ (a b : α), a * b = a * b
• lt_norm_lt : ∀ (x y : ), 0 xx < y∃ (a : α), x < a a < y

The range of the norm is dense in the collection of nonnegative real numbers.

Instances
theorem DenselyNormedField.lt_norm_lt {α : Type u_5} [self : ] (x : ) (y : ) :
0 xx < y∃ (a : α), x < a a < y

The range of the norm is dense in the collection of nonnegative real numbers.

@[instance 100]

A densely normed field is always a nontrivially normed field. See note [lower instance priority].

Equations
• DenselyNormedField.toNontriviallyNormedField =
@[instance 100]
instance NormedField.toNormedDivisionRing {α : Type u_1} [] :
Equations
• NormedField.toNormedDivisionRing = let __src := inst;
@[instance 100]
instance NormedField.toNormedCommRing {α : Type u_1} [] :
Equations
• NormedField.toNormedCommRing = let __src := inst;
@[simp]
theorem norm_prod {α : Type u_1} {β : Type u_2} [] (s : ) (f : βα) :
bs, f b = bs, f b
@[simp]
theorem nnnorm_prod {α : Type u_1} {β : Type u_2} [] (s : ) (f : βα) :
bs, f b‖₊ = bs, f b‖₊
theorem NormedField.exists_one_lt_norm (α : Type u_1) :
∃ (x : α), 1 < x
theorem NormedField.exists_lt_norm (α : Type u_1) (r : ) :
∃ (x : α), r < x
theorem NormedField.exists_norm_lt (α : Type u_1) {r : } (hr : 0 < r) :
∃ (x : α), 0 < x x < r
theorem NormedField.exists_norm_lt_one (α : Type u_1) :
∃ (x : α), 0 < x x < 1
theorem NormedField.punctured_nhds_neBot {α : Type u_1} (x : α) :
(nhdsWithin x {x}).NeBot
theorem NormedField.nhdsWithin_isUnit_neBot {α : Type u_1} :
(nhdsWithin 0 {x : α | }).NeBot
theorem NormedField.exists_lt_norm_lt (α : Type u_1) {r₁ : } {r₂ : } (h₀ : 0 r₁) (h : r₁ < r₂) :
∃ (x : α), r₁ < x x < r₂
theorem NormedField.exists_lt_nnnorm_lt (α : Type u_1) {r₁ : NNReal} {r₂ : NNReal} (h : r₁ < r₂) :
∃ (x : α), r₁ < x‖₊ x‖₊ < r₂
Equations
• =
Equations
• =
def NontriviallyNormedField.ofNormNeOne {𝕜 : Type u_5} [h' : ] (h : ∃ (x : 𝕜), x 0 x 1) :

A normed field is nontrivially normed provided that the norm of some nonzero element is not one.

Equations
Instances For
Equations
noncomputable instance Real.normedField :
Equations
noncomputable instance Real.denselyNormedField :
Equations
theorem Real.toNNReal_mul_nnnorm {x : } (y : ) (hx : 0 x) :
x.toNNReal * y‖₊ = x * y‖₊
theorem Real.nnnorm_mul_toNNReal (x : ) {y : } (hy : 0 y) :
x‖₊ * y.toNNReal = x * y‖₊
theorem NNReal.norm_eq (x : NNReal) :
x = x
@[simp]
theorem NNReal.nnnorm_eq (x : NNReal) :
x‖₊ = x
theorem NNReal.lipschitzWith_sub :
LipschitzWith 2 fun (p : ) => p.1 - p.2
@[simp]
theorem norm_norm {α : Type u_1} (x : α) :
@[simp]
theorem nnnorm_norm {α : Type u_1} (a : α) :
theorem NormedAddCommGroup.tendsto_atTop {α : Type u_1} [] [] {β : Type u_5} {f : αβ} {b : β} :
Filter.Tendsto f Filter.atTop (nhds b) ∀ (ε : ), 0 < ε∃ (N : α), ∀ (n : α), N nf n - b < ε

A restatement of MetricSpace.tendsto_atTop in terms of the norm.

theorem NormedAddCommGroup.tendsto_atTop' {α : Type u_1} [] [] [] {β : Type u_5} {f : αβ} {b : β} :
Filter.Tendsto f Filter.atTop (nhds b) ∀ (ε : ), 0 < ε∃ (N : α), ∀ (n : α), N < nf n - b < ε

A variant of NormedAddCommGroup.tendsto_atTop that uses ∃ N, ∀ n > N, ... rather than ∃ N, ∀ n ≥ N, ...

Equations
Equations
Equations
class RingHomIsometric {R₁ : Type u_5} {R₂ : Type u_6} [Semiring R₁] [Semiring R₂] [Norm R₁] [Norm R₂] (σ : R₁ →+* R₂) :

This class states that a ring homomorphism is isometric. This is a sufficient assumption for a continuous semilinear map to be bounded and this is the main use for this typeclass.

• is_iso : ∀ {x : R₁}, σ x = x

The ring homomorphism is an isometry.

Instances
@[simp]
theorem RingHomIsometric.is_iso {R₁ : Type u_5} {R₂ : Type u_6} [Semiring R₁] [Semiring R₂] [Norm R₁] [Norm R₂] {σ : R₁ →+* R₂} [self : ] {x : R₁} :

The ring homomorphism is an isometry.

instance RingHomIsometric.ids {R₁ : Type u_5} [] :
Equations
• =

### Induced normed structures #

@[reducible, inline]
abbrev NonUnitalSeminormedRing.induced {F : Type u_5} (R : Type u_6) (S : Type u_7) [FunLike F R S] [] [] (f : F) :

A non-unital ring homomorphism from a NonUnitalRing to a NonUnitalSeminormedRing induces a NonUnitalSeminormedRing structure on the domain.

See note [reducible non-instances]

Equations
• = let __src := ; let __src_1 := inst✝¹;
Instances For
@[reducible, inline]
abbrev NonUnitalNormedRing.induced {F : Type u_5} (R : Type u_6) (S : Type u_7) [FunLike F R S] [] [] (f : F) (hf : ) :

An injective non-unital ring homomorphism from a NonUnitalRing to a NonUnitalNormedRing induces a NonUnitalNormedRing structure on the domain.

See note [reducible non-instances]

Equations
• = let __src := ; let __src_1 := ;
Instances For
@[reducible, inline]
abbrev SeminormedRing.induced {F : Type u_5} (R : Type u_6) (S : Type u_7) [FunLike F R S] [Ring R] [] [] (f : F) :

A non-unital ring homomorphism from a Ring to a SeminormedRing induces a SeminormedRing structure on the domain.

See note [reducible non-instances]

Equations
• = let __src := ; let __src_1 := ; let __src_2 := inst✝¹;
Instances For
@[reducible, inline]
abbrev NormedRing.induced {F : Type u_5} (R : Type u_6) (S : Type u_7) [FunLike F R S] [Ring R] [] [] (f : F) (hf : ) :

An injective non-unital ring homomorphism from a Ring to a NormedRing induces a NormedRing structure on the domain.

See note [reducible non-instances]

Equations
Instances For
@[reducible, inline]
abbrev NonUnitalSeminormedCommRing.induced {F : Type u_5} (R : Type u_6) (S : Type u_7) [FunLike F R S] [] (f : F) :

A non-unital ring homomorphism from a NonUnitalCommRing to a NonUnitalSeminormedCommRing induces a NonUnitalSeminormedCommRing structure on the domain.

See note [reducible non-instances]

Equations
• = let __src := ; let __src_1 := inst✝¹;
Instances For
@[reducible, inline]
abbrev NonUnitalNormedCommRing.induced {F : Type u_5} (R : Type u_6) (S : Type u_7) [FunLike F R S] [] (f : F) (hf : ) :

An injective non-unital ring homomorphism from a NonUnitalCommRing to a NonUnitalNormedCommRing induces a NonUnitalNormedCommRing structure on the domain.

See note [reducible non-instances]

Equations
• = let __src := ; let __src_1 := inst✝¹;
Instances For
@[reducible, inline]
abbrev SeminormedCommRing.induced {F : Type u_5} (R : Type u_6) (S : Type u_7) [FunLike F R S] [] [] [] (f : F) :

A non-unital ring homomorphism from a CommRing to a SeminormedRing induces a SeminormedCommRing structure on the domain.

See note [reducible non-instances]

Equations
• = let __src := ; let __src_1 := ; let __src_2 := inst✝¹;
Instances For
@[reducible, inline]
abbrev NormedCommRing.induced {F : Type u_5} (R : Type u_6) (S : Type u_7) [FunLike F R S] [] [] [] (f : F) (hf : ) :

An injective non-unital ring homomorphism from a CommRing to a NormedRing induces a NormedCommRing structure on the domain.

See note [reducible non-instances]

Equations
• = let __src := ; let __src_1 := ;
Instances For
@[reducible, inline]
abbrev NormedDivisionRing.induced {F : Type u_5} (R : Type u_6) (S : Type u_7) [FunLike F R S] [] [] (f : F) (hf : ) :

An injective non-unital ring homomorphism from a DivisionRing to a NormedRing induces a NormedDivisionRing structure on the domain.

See note [reducible non-instances]

Equations
• = let __src := ; let __src_1 := inst✝¹;
Instances For
@[reducible, inline]
abbrev NormedField.induced {F : Type u_5} (R : Type u_6) (S : Type u_7) [FunLike F R S] [] [] [] (f : F) (hf : ) :

An injective non-unital ring homomorphism from a Field to a NormedRing induces a NormedField structure on the domain.

See note [reducible non-instances]

Equations
Instances For
theorem NormOneClass.induced {F : Type u_8} (R : Type u_9) (S : Type u_10) [Ring R] [] [] [FunLike F R S] [RingHomClass F R S] (f : F) :

A ring homomorphism from a Ring R to a SeminormedRing S which induces the norm structure SeminormedRing.induced makes R satisfy ‖(1 : R)‖ = 1 whenever ‖(1 : S)‖ = 1.

instance SubringClass.toSeminormedRing {S : Type u_5} {R : Type u_6} [SetLike S R] [] [] (s : S) :
Equations
instance SubringClass.toNormedRing {S : Type u_5} {R : Type u_6} [SetLike S R] [] [] (s : S) :
Equations
instance SubringClass.toSeminormedCommRing {S : Type u_5} {R : Type u_6} [SetLike S R] [_h : ] (s : S) :
Equations
• = let __src := ;
instance SubringClass.toNormedCommRing {S : Type u_5} {R : Type u_6} [SetLike S R] [] [] (s : S) :
Equations
• = let __src := ;