Normed rings

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

A normed ring instance can be constructed from a given real absolute value on a ring via AbsoluteValue.toNormedRing.

class NonUnitalSeminormedRing (α : Type u_5) extends Norm α, NonUnitalRing α, PseudoMetricSpace α : 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 : α → α → α
• 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 : α) : AddMonoid.nsmul 0 x = 0
• nsmul_succ (n : ℕ) (x : α) : AddMonoid.nsmul (n + 1) x = AddMonoid.nsmul n x + x
• neg : α → α
• sub : α → α → α
• sub_eq_add_neg (a b : α) : a - b = a + -b
• zsmul : ℤ → α → α
• zsmul_zero' (a : α) : SubNegMonoid.zsmul 0 a = 0
• zsmul_succ' (n : ℕ) (a : α) : SubNegMonoid.zsmul (↑n.succ) a = SubNegMonoid.zsmul (↑n) a + a
• zsmul_neg' (n : ℕ) (a : α) : SubNegMonoid.zsmul (Int.negSucc n) a = -SubNegMonoid.zsmul (↑n.succ) a
• neg_add_cancel (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 : α) : edist x y = ENNReal.ofReal (dist x y)
• toUniformSpace : UniformSpace α
• uniformity_dist : uniformity α = ⨅ (ε : ℝ), ⨅ (_ : ε > 0), Filter.principal {p : α × α | dist p.1 p.2 < ε}
• toBornology : Bornology α
• cobounded_sets : (Bornology.cobounded α).sets = {s : Set α | ∃ (C : ℝ), ∀ x ∈ sᶜ, ∀ y ∈ sᶜ, dist x y ≤ C}
• dist_eq (x y : α) : dist x y = ‖x - y‖

  The distance is induced by the norm.

• norm_mul_le (a b : α) : ‖a * b‖ ≤ ‖a‖ * ‖b‖

  The norm is submultiplicative.

Instances

• BoundedContinuousFunction.instNonUnitalSeminormedRing
• ContinuousMap.instNonUnitalSeminormedRing
• MulOpposite.instNonUnitalSeminormedRing
• NonUnitalNormedRing.toNonUnitalSeminormedRing
• NonUnitalSubalgebra.nonUnitalSeminormedRing
• NonUnitalSubalgebraClass.nonUnitalSeminormedRing
• Pi.nonUnitalSeminormedRing
• Prod.nonUnitalSeminormedRing
• SeminormedRing.toNonUnitalSeminormedRing
• ULift.nonUnitalSeminormedRing
• instNonUnitalSeminormedRingRestrictScalars

class SeminormedRing (α : Type u_5) extends Norm α, Ring α, PseudoMetricSpace α : Type u_5

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

• norm : α → ℝ
• add : α → α → α
• 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 : α) : AddMonoid.nsmul 0 x = 0
• nsmul_succ (n : ℕ) (x : α) : AddMonoid.nsmul (n + 1) x = AddMonoid.nsmul n 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.natCast 0 = 0
• natCast_succ (n : ℕ) : NatCast.natCast (n + 1) = NatCast.natCast n + 1
• npow : ℕ → α → α
• npow_zero (x : α) : Semiring.npow 0 x = 1
• npow_succ (n : ℕ) (x : α) : Semiring.npow (n + 1) x = Semiring.npow n x * x
• neg : α → α
• sub : α → α → α
• sub_eq_add_neg (a b : α) : a - b = a + -b
• zsmul : ℤ → α → α
• zsmul_zero' (a : α) : Ring.zsmul 0 a = 0
• zsmul_succ' (n : ℕ) (a : α) : Ring.zsmul (↑n.succ) a = Ring.zsmul (↑n) a + a
• zsmul_neg' (n : ℕ) (a : α) : Ring.zsmul (Int.negSucc n) a = -Ring.zsmul (↑n.succ) a
• neg_add_cancel (a : α) : -a + a = 0
• intCast : ℤ → α
• intCast_ofNat (n : ℕ) : IntCast.intCast ↑n = ↑n
• intCast_negSucc (n : ℕ) : IntCast.intCast (Int.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 : α) : edist x y = ENNReal.ofReal (dist x y)
• toUniformSpace : UniformSpace α
• uniformity_dist : uniformity α = ⨅ (ε : ℝ), ⨅ (_ : ε > 0), Filter.principal {p : α × α | dist p.1 p.2 < ε}
• toBornology : Bornology α
• cobounded_sets : (Bornology.cobounded α).sets = {s : Set α | ∃ (C : ℝ), ∀ x ∈ sᶜ, ∀ y ∈ sᶜ, dist x y ≤ C}
• dist_eq (x y : α) : dist x y = ‖x - y‖

  The distance is induced by the norm.

• norm_mul_le (a b : α) : ‖a * b‖ ≤ ‖a‖ * ‖b‖

  The norm is submultiplicative.

Instances

• BoundedContinuousFunction.instSeminormedRing
• ContinuousLinearMap.toSeminormedRing
• ContinuousMap.instSeminormedRing
• MulOpposite.instSeminormedRing
• NormedRing.toSeminormedRing
• Pi.seminormedRing
• Prod.seminormedRing
• Subalgebra.seminormedRing
• SubalgebraClass.seminormedRing
• SubringClass.toSeminormedRing
• ULift.seminormedRing
• instSeminormedRingRestrictScalars

@[instance 100]

instance SeminormedRing.toNonUnitalSeminormedRing {α : Type u_2} [β : SeminormedRing α] : NonUnitalSeminormedRing α

A seminormed ring is a non-unital seminormed ring.

Equations

• SeminormedRing.toNonUnitalSeminormedRing = NonUnitalSeminormedRing.mk ⋯ ⋯

class NonUnitalNormedRing (α : Type u_5) extends Norm α, NonUnitalRing α, MetricSpace α : 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 : α → α → α
• 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 : α) : AddMonoid.nsmul 0 x = 0
• nsmul_succ (n : ℕ) (x : α) : AddMonoid.nsmul (n + 1) x = AddMonoid.nsmul n x + x
• neg : α → α
• sub : α → α → α
• sub_eq_add_neg (a b : α) : a - b = a + -b
• zsmul : ℤ → α → α
• zsmul_zero' (a : α) : SubNegMonoid.zsmul 0 a = 0
• zsmul_succ' (n : ℕ) (a : α) : SubNegMonoid.zsmul (↑n.succ) a = SubNegMonoid.zsmul (↑n) a + a
• zsmul_neg' (n : ℕ) (a : α) : SubNegMonoid.zsmul (Int.negSucc n) a = -SubNegMonoid.zsmul (↑n.succ) a
• neg_add_cancel (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 : α) : edist x y = ENNReal.ofReal (dist x y)
• toUniformSpace : UniformSpace α
• uniformity_dist : uniformity α = ⨅ (ε : ℝ), ⨅ (_ : ε > 0), Filter.principal {p : α × α | dist p.1 p.2 < ε}
• toBornology : Bornology α
• cobounded_sets : (Bornology.cobounded α).sets = {s : Set α | ∃ (C : ℝ), ∀ x ∈ sᶜ, ∀ y ∈ sᶜ, dist x y ≤ C}
• eq_of_dist_eq_zero {x y : α} : dist x y = 0 → x = y
• dist_eq (x y : α) : dist x y = ‖x - y‖

  The distance is induced by the norm.

• norm_mul_le (a b : α) : ‖a * b‖ ≤ ‖a‖ * ‖b‖

  The norm is submultiplicative.

Instances

• BoundedContinuousFunction.instNonUnitalNormedRing
• ContinuousMap.instNonUnitalNormedRing
• MulOpposite.instNonUnitalNormedRing
• NonUnitalSubalgebra.nonUnitalNormedRing
• NonUnitalSubalgebraClass.nonUnitalNormedRing
• NormedRing.toNonUnitalNormedRing
• Pi.nonUnitalNormedRing
• Prod.nonUnitalNormedRing
• SeparationQuotient.instNonUnitalNormedRing
• ULift.nonUnitalNormedRing
• instNonUnitalNormedRingRestrictScalars

@[instance 100]

instance NonUnitalNormedRing.toNonUnitalSeminormedRing {α : Type u_2} [β : NonUnitalNormedRing α] : NonUnitalSeminormedRing α

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

Equations

• NonUnitalNormedRing.toNonUnitalSeminormedRing = NonUnitalSeminormedRing.mk ⋯ ⋯

class NormedRing (α : Type u_5) extends Norm α, Ring α, MetricSpace α : Type u_5

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

• norm : α → ℝ
• add : α → α → α
• 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 : α) : AddMonoid.nsmul 0 x = 0
• nsmul_succ (n : ℕ) (x : α) : AddMonoid.nsmul (n + 1) x = AddMonoid.nsmul n 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.natCast 0 = 0
• natCast_succ (n : ℕ) : NatCast.natCast (n + 1) = NatCast.natCast n + 1
• npow : ℕ → α → α
• npow_zero (x : α) : Semiring.npow 0 x = 1
• npow_succ (n : ℕ) (x : α) : Semiring.npow (n + 1) x = Semiring.npow n x * x
• neg : α → α
• sub : α → α → α
• sub_eq_add_neg (a b : α) : a - b = a + -b
• zsmul : ℤ → α → α
• zsmul_zero' (a : α) : Ring.zsmul 0 a = 0
• zsmul_succ' (n : ℕ) (a : α) : Ring.zsmul (↑n.succ) a = Ring.zsmul (↑n) a + a
• zsmul_neg' (n : ℕ) (a : α) : Ring.zsmul (Int.negSucc n) a = -Ring.zsmul (↑n.succ) a
• neg_add_cancel (a : α) : -a + a = 0
• intCast : ℤ → α
• intCast_ofNat (n : ℕ) : IntCast.intCast ↑n = ↑n
• intCast_negSucc (n : ℕ) : IntCast.intCast (Int.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 : α) : edist x y = ENNReal.ofReal (dist x y)
• toUniformSpace : UniformSpace α
• uniformity_dist : uniformity α = ⨅ (ε : ℝ), ⨅ (_ : ε > 0), Filter.principal {p : α × α | dist p.1 p.2 < ε}
• toBornology : Bornology α
• cobounded_sets : (Bornology.cobounded α).sets = {s : Set α | ∃ (C : ℝ), ∀ x ∈ sᶜ, ∀ y ∈ sᶜ, dist x y ≤ C}
• eq_of_dist_eq_zero {x y : α} : dist x y = 0 → x = y
• dist_eq (x y : α) : dist x y = ‖x - y‖

  The distance is induced by the norm.

• norm_mul_le (a b : α) : ‖a * b‖ ≤ ‖a‖ * ‖b‖

  The norm is submultiplicative.

Instances

• BoundedContinuousFunction.instNormedRing
• ContinuousLinearMap.toNormedRing
• ContinuousMap.instNormedRing
• MulOpposite.instNormedRing
• NormedDivisionRing.toNormedRing
• Pi.normedRing
• Prod.normedRing
• SeparationQuotient.instNormedRing
• Subalgebra.normedRing
• SubalgebraClass.normedRing
• SubringClass.toNormedRing
• ULift.normedRing
• UniformSpace.Completion.instNormedRing
• WithAbs.normedRing
• instNormedRingRestrictScalars

@[instance 100]

instance NormedRing.toSeminormedRing {α : Type u_2} [β : NormedRing α] : SeminormedRing α

A normed ring is a seminormed ring.

Equations

• NormedRing.toSeminormedRing = SeminormedRing.mk ⋯ ⋯

@[instance 100]

instance NormedRing.toNonUnitalNormedRing {α : Type u_2} [β : NormedRing α] : NonUnitalNormedRing α

A normed ring is a non-unital normed ring.

Equations

• NormedRing.toNonUnitalNormedRing = NonUnitalNormedRing.mk ⋯ ⋯

class NonUnitalSeminormedCommRing (α : Type u_5) extends NonUnitalSeminormedRing α, NonUnitalCommRing α : 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 : α → α → α
• 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 : α) : AddMonoid.nsmul 0 x = 0
• nsmul_succ (n : ℕ) (x : α) : AddMonoid.nsmul (n + 1) x = AddMonoid.nsmul n x + x
• neg : α → α
• sub : α → α → α
• sub_eq_add_neg (a b : α) : a - b = a + -b
• zsmul : ℤ → α → α
• zsmul_zero' (a : α) : SubNegMonoid.zsmul 0 a = 0
• zsmul_succ' (n : ℕ) (a : α) : SubNegMonoid.zsmul (↑n.succ) a = SubNegMonoid.zsmul (↑n) a + a
• zsmul_neg' (n : ℕ) (a : α) : SubNegMonoid.zsmul (Int.negSucc n) a = -SubNegMonoid.zsmul (↑n.succ) a
• neg_add_cancel (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 : α) : edist x y = ENNReal.ofReal (dist x y)
• toUniformSpace : UniformSpace α
• uniformity_dist : uniformity α = ⨅ (ε : ℝ), ⨅ (_ : ε > 0), Filter.principal {p : α × α | dist p.1 p.2 < ε}
• toBornology : Bornology α
• cobounded_sets : (Bornology.cobounded α).sets = {s : Set α | ∃ (C : ℝ), ∀ x ∈ sᶜ, ∀ y ∈ sᶜ, dist x y ≤ C}
• dist_eq (x y : α) : dist x y = ‖x - y‖
• norm_mul_le (a b : α) : ‖a * b‖ ≤ ‖a‖ * ‖b‖
• mul_comm (a b : α) : a * b = b * a

Instances

• BoundedContinuousFunction.instNonUnitalSeminormedCommRing
• ContinuousMap.instNonUnitalSeminormedCommRing
• MulOpposite.instNonUnitalSeminormedCommRing
• NonUnitalNormedCommRing.toNonUnitalSeminormedCommRing
• NonUnitalSubalgebra.nonUnitalSeminormedCommRing
• Pi.nonUnitalSeminormedCommRing
• Prod.nonUnitalSeminormedCommRing
• SeminormedCommRing.toNonUnitalSeminormedCommRing
• ULift.nonUnitalSeminormedCommRing
• instNonUnitalSeminormedCommRingRestrictScalars

class NonUnitalNormedCommRing (α : Type u_5) extends NonUnitalNormedRing α, NonUnitalCommRing α : 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 : α → α → α
• 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 : α) : AddMonoid.nsmul 0 x = 0
• nsmul_succ (n : ℕ) (x : α) : AddMonoid.nsmul (n + 1) x = AddMonoid.nsmul n x + x
• neg : α → α
• sub : α → α → α
• sub_eq_add_neg (a b : α) : a - b = a + -b
• zsmul : ℤ → α → α
• zsmul_zero' (a : α) : SubNegMonoid.zsmul 0 a = 0
• zsmul_succ' (n : ℕ) (a : α) : SubNegMonoid.zsmul (↑n.succ) a = SubNegMonoid.zsmul (↑n) a + a
• zsmul_neg' (n : ℕ) (a : α) : SubNegMonoid.zsmul (Int.negSucc n) a = -SubNegMonoid.zsmul (↑n.succ) a
• neg_add_cancel (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 : α) : edist x y = ENNReal.ofReal (dist x y)
• toUniformSpace : UniformSpace α
• uniformity_dist : uniformity α = ⨅ (ε : ℝ), ⨅ (_ : ε > 0), Filter.principal {p : α × α | dist p.1 p.2 < ε}
• toBornology : Bornology α
• cobounded_sets : (Bornology.cobounded α).sets = {s : Set α | ∃ (C : ℝ), ∀ x ∈ sᶜ, ∀ y ∈ sᶜ, dist x y ≤ C}
• eq_of_dist_eq_zero {x y : α} : dist x y = 0 → x = y
• dist_eq (x y : α) : dist x y = ‖x - y‖
• norm_mul_le (a b : α) : ‖a * b‖ ≤ ‖a‖ * ‖b‖
• mul_comm (a b : α) : a * b = b * a

Instances

• BoundedContinuousFunction.instNonUnitalNormedCommRing
• ContinuousMap.instNonUnitalNormedCommRing
• ContinuousMapZero.instNonUnitalNormedCommRing
• MulOpposite.instNonUnitalNormedCommRing
• NonUnitalSubalgebra.nonUnitalNormedCommRing
• NormedCommRing.toNonUnitalNormedCommRing
• Pi.nonUnitalNormedCommRing
• Prod.nonUnitalNormedCommRing
• SeparationQuotient.instNonUnitalNormedCommRing
• ULift.nonUnitalNormedCommRing
• instNonUnitalNormedCommRingRestrictScalars

@[instance 100]

instance NonUnitalNormedCommRing.toNonUnitalSeminormedCommRing {α : Type u_2} [β : NonUnitalNormedCommRing α] : NonUnitalSeminormedCommRing α

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

Equations

• NonUnitalNormedCommRing.toNonUnitalSeminormedCommRing = NonUnitalSeminormedCommRing.mk ⋯

class SeminormedCommRing (α : Type u_5) extends SeminormedRing α, CommRing α : 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 : α → α → α
• 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 : α) : AddMonoid.nsmul 0 x = 0
• nsmul_succ (n : ℕ) (x : α) : AddMonoid.nsmul (n + 1) x = AddMonoid.nsmul n 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.natCast 0 = 0
• natCast_succ (n : ℕ) : NatCast.natCast (n + 1) = NatCast.natCast n + 1
• npow : ℕ → α → α
• npow_zero (x : α) : Semiring.npow 0 x = 1
• npow_succ (n : ℕ) (x : α) : Semiring.npow (n + 1) x = Semiring.npow n x * x
• neg : α → α
• sub : α → α → α
• sub_eq_add_neg (a b : α) : a - b = a + -b
• zsmul : ℤ → α → α
• zsmul_zero' (a : α) : Ring.zsmul 0 a = 0
• zsmul_succ' (n : ℕ) (a : α) : Ring.zsmul (↑n.succ) a = Ring.zsmul (↑n) a + a
• zsmul_neg' (n : ℕ) (a : α) : Ring.zsmul (Int.negSucc n) a = -Ring.zsmul (↑n.succ) a
• neg_add_cancel (a : α) : -a + a = 0
• intCast : ℤ → α
• intCast_ofNat (n : ℕ) : IntCast.intCast ↑n = ↑n
• intCast_negSucc (n : ℕ) : IntCast.intCast (Int.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 : α) : edist x y = ENNReal.ofReal (dist x y)
• toUniformSpace : UniformSpace α
• uniformity_dist : uniformity α = ⨅ (ε : ℝ), ⨅ (_ : ε > 0), Filter.principal {p : α × α | dist p.1 p.2 < ε}
• toBornology : Bornology α
• cobounded_sets : (Bornology.cobounded α).sets = {s : Set α | ∃ (C : ℝ), ∀ x ∈ sᶜ, ∀ y ∈ sᶜ, dist x y ≤ C}
• dist_eq (x y : α) : dist x y = ‖x - y‖
• norm_mul_le (a b : α) : ‖a * b‖ ≤ ‖a‖ * ‖b‖
• mul_comm (a b : α) : a * b = b * a

Instances

• BoundedContinuousFunction.instSeminormedCommRing
• ContinuousMap.instSeminormedCommRing
• Ideal.Quotient.semiNormedCommRing
• MulOpposite.instSeminormedCommRing
• NormedCommRing.toSeminormedCommRing
• Pi.seminormedCommRing
• Prod.seminormedCommRing
• Subalgebra.seminormedCommRing
• SubringClass.toSeminormedCommRing
• ULift.seminormedCommRing
• instSeminormedCommRingRestrictScalars

class NormedCommRing (α : Type u_5) extends NormedRing α, CommRing α : 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 : α → α → α
• 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 : α) : AddMonoid.nsmul 0 x = 0
• nsmul_succ (n : ℕ) (x : α) : AddMonoid.nsmul (n + 1) x = AddMonoid.nsmul n 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.natCast 0 = 0
• natCast_succ (n : ℕ) : NatCast.natCast (n + 1) = NatCast.natCast n + 1
• npow : ℕ → α → α
• npow_zero (x : α) : Semiring.npow 0 x = 1
• npow_succ (n : ℕ) (x : α) : Semiring.npow (n + 1) x = Semiring.npow n x * x
• neg : α → α
• sub : α → α → α
• sub_eq_add_neg (a b : α) : a - b = a + -b
• zsmul : ℤ → α → α
• zsmul_zero' (a : α) : Ring.zsmul 0 a = 0
• zsmul_succ' (n : ℕ) (a : α) : Ring.zsmul (↑n.succ) a = Ring.zsmul (↑n) a + a
• zsmul_neg' (n : ℕ) (a : α) : Ring.zsmul (Int.negSucc n) a = -Ring.zsmul (↑n.succ) a
• neg_add_cancel (a : α) : -a + a = 0
• intCast : ℤ → α
• intCast_ofNat (n : ℕ) : IntCast.intCast ↑n = ↑n
• intCast_negSucc (n : ℕ) : IntCast.intCast (Int.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 : α) : edist x y = ENNReal.ofReal (dist x y)
• toUniformSpace : UniformSpace α
• uniformity_dist : uniformity α = ⨅ (ε : ℝ), ⨅ (_ : ε > 0), Filter.principal {p : α × α | dist p.1 p.2 < ε}
• toBornology : Bornology α
• cobounded_sets : (Bornology.cobounded α).sets = {s : Set α | ∃ (C : ℝ), ∀ x ∈ sᶜ, ∀ y ∈ sᶜ, dist x y ≤ C}
• eq_of_dist_eq_zero {x y : α} : dist x y = 0 → x = y
• dist_eq (x y : α) : dist x y = ‖x - y‖
• norm_mul_le (a b : α) : ‖a * b‖ ≤ ‖a‖ * ‖b‖
• mul_comm (a b : α) : a * b = b * a

Instances

• BoundedContinuousFunction.instNormedCommRing
• ContinuousMap.instNormedCommRing
• Ideal.Quotient.normedCommRing
• Int.instNormedCommRing
• MulOpposite.instNormedCommRing
• NormedField.toNormedCommRing
• PUnit.normedCommRing
• PadicInt.instNormedCommRing
• Pi.normedCommutativeRing
• Prod.normedCommRing
• Real.normedCommRing
• SeparationQuotient.instNormedCommRing
• Subalgebra.normedCommRing
• SubringClass.toNormedCommRing
• ULift.normedCommRing
• UniformSpace.Completion.instNormedCommRing
• instNormedCommRingRestrictScalars

@[instance 100]

instance SeminormedCommRing.toNonUnitalSeminormedCommRing {α : Type u_2} [β : SeminormedCommRing α] : NonUnitalSeminormedCommRing α

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

Equations

• SeminormedCommRing.toNonUnitalSeminormedCommRing = NonUnitalSeminormedCommRing.mk ⋯

@[instance 100]

instance NormedCommRing.toNonUnitalNormedCommRing {α : Type u_2} [β : NormedCommRing α] : NonUnitalNormedCommRing α

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

Equations

• NormedCommRing.toNonUnitalNormedCommRing = NonUnitalNormedCommRing.mk ⋯

@[instance 100]

instance NormedCommRing.toSeminormedCommRing {α : Type u_2} [β : NormedCommRing α] : SeminormedCommRing α

A normed commutative ring is a seminormed commutative ring.

Equations

• NormedCommRing.toSeminormedCommRing = SeminormedCommRing.mk ⋯

instance PUnit.normedCommRing : NormedCommRing PUnit.{u_5 + 1}

Equations

• PUnit.normedCommRing = NormedCommRing.mk ⋯

class NormOneClass (α : Type u_5) [Norm α] [One α] : Prop

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

• BoundedContinuousFunction.instNormOneClass
• CStarRing.instNormOneClassOfNontrivial
• ContinuousLinearMap.normOneClass
• ContinuousMap.instNormOneClassOfNonempty
• Int.instNormOneClass
• Matrix.instNormOneClassOfNonempty
• Matrix.linfty_opNormOneClass
• MulOpposite.normOneClass
• NormedDivisionRing.to_normOneClass
• PadicInt.instNormOneClass
• Pi.normOneClass
• Prod.normOneClass
• Quaternion.instNormOneClassReal
• SeparationQuotient.instNormOneClass
• SubringClass.toNormOneClass
• ULift.normOneClass

@[simp]

theorem nnnorm_one {G : Type u_1} [SeminormedAddCommGroup G] [One G] [NormOneClass G] : ‖1‖₊ = 1

@[simp]

theorem enorm_one {G : Type u_1} [SeminormedAddCommGroup G] [One G] [NormOneClass G] : ‖1‖ₑ = 1

theorem NormOneClass.nontrivial {G : Type u_1} [SeminormedAddCommGroup G] [One G] [NormOneClass G] : Nontrivial G

@[instance 100]

instance NonUnitalNormedRing.toNormedAddCommGroup {α : Type u_2} [β : NonUnitalNormedRing α] : NormedAddCommGroup α

Equations

• NonUnitalNormedRing.toNormedAddCommGroup = NormedAddCommGroup.mk ⋯

@[instance 100]

instance NonUnitalSeminormedRing.toSeminormedAddCommGroup {α : Type u_2} [NonUnitalSeminormedRing α] : SeminormedAddCommGroup α

Equations

• NonUnitalSeminormedRing.toSeminormedAddCommGroup = SeminormedAddCommGroup.mk ⋯

instance ULift.normOneClass {α : Type u_2} [SeminormedAddCommGroup α] [One α] [NormOneClass α] : NormOneClass (ULift.{u_5, u_2} α)

instance Prod.normOneClass {α : Type u_2} {β : Type u_3} [SeminormedAddCommGroup α] [One α] [NormOneClass α] [SeminormedAddCommGroup β] [One β] [NormOneClass β] : NormOneClass (α × β)

instance Pi.normOneClass {ι : Type u_5} {α : ι → Type u_6} [Nonempty ι] [Fintype ι] [(i : ι) → SeminormedAddCommGroup (α i)] [(i : ι) → One (α i)] [∀ (i : ι), NormOneClass (α i)] : NormOneClass ((i : ι) → α i)

instance MulOpposite.normOneClass {α : Type u_2} [SeminormedAddCommGroup α] [One α] [NormOneClass α] : NormOneClass αᵐᵒᵖ

theorem norm_mul_le {α : Type u_2} [NonUnitalSeminormedRing α] (a b : α) : ‖a * b‖ ≤ ‖a‖ * ‖b‖

The norm is submultiplicative.

theorem nnnorm_mul_le {α : Type u_2} [NonUnitalSeminormedRing α] (a b : α) : ‖a * b‖₊ ≤ ‖a‖₊ * ‖b‖₊

theorem norm_mul_le_of_le {α : Type u_2} [NonUnitalSeminormedRing α] {a₁ a₂ : α} {r₁ r₂ : ℝ} (h₁ : ‖a₁‖ ≤ r₁) (h₂ : ‖a₂‖ ≤ r₂) : ‖a₁ * a₂‖ ≤ r₁ * r₂

theorem nnnorm_mul_le_of_le {α : Type u_2} [NonUnitalSeminormedRing α] {a₁ a₂ : α} {r₁ r₂ : NNReal} (h₁ : ‖a₁‖₊ ≤ r₁) (h₂ : ‖a₂‖₊ ≤ r₂) : ‖a₁ * a₂‖₊ ≤ r₁ * r₂

theorem norm_mul₃_le {α : Type u_2} [NonUnitalSeminormedRing α] {a b c : α} : ‖a * b * c‖ ≤ ‖a‖ * ‖b‖ * ‖c‖

theorem nnnorm_mul₃_le {α : Type u_2} [NonUnitalSeminormedRing α] {a b c : α} : ‖a * b * c‖₊ ≤ ‖a‖₊ * ‖b‖₊ * ‖c‖₊

theorem one_le_norm_one (β : Type u_5) [NormedRing β] [Nontrivial β] : 1 ≤ ‖1‖

theorem one_le_nnnorm_one (β : Type u_5) [NormedRing β] [Nontrivial β] : 1 ≤ ‖1‖₊

theorem mulLeft_bound {α : Type u_2} [NonUnitalSeminormedRing α] (x y : α) : ‖(AddMonoidHom.mulLeft x) y‖ ≤ ‖x‖ * ‖y‖

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

theorem mulRight_bound {α : Type u_2} [NonUnitalSeminormedRing α] (x y : α) : ‖(AddMonoidHom.mulRight x) y‖ ≤ ‖x‖ * ‖y‖

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

instance NonUnitalSubalgebra.nonUnitalSeminormedRing {𝕜 : Type u_5} [CommRing 𝕜] {E : Type u_6} [NonUnitalSeminormedRing E] [Module 𝕜 E] (s : NonUnitalSubalgebra 𝕜 E) : NonUnitalSeminormedRing ↥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 = NonUnitalSeminormedRing.mk ⋯ ⋯

@[instance 75]

instance NonUnitalSubalgebraClass.nonUnitalSeminormedRing {S : Type u_5} {𝕜 : Type u_6} {E : Type u_7} [CommRing 𝕜] [NonUnitalSeminormedRing E] [Module 𝕜 E] [SetLike S E] [NonUnitalSubringClass S E] [SMulMemClass S 𝕜 E] (s : S) : NonUnitalSeminormedRing ↥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

• NonUnitalSubalgebraClass.nonUnitalSeminormedRing s = NonUnitalSeminormedRing.mk ⋯ ⋯

instance NonUnitalSubalgebra.nonUnitalNormedRing {𝕜 : Type u_5} [CommRing 𝕜] {E : Type u_6} [NonUnitalNormedRing E] [Module 𝕜 E] (s : NonUnitalSubalgebra 𝕜 E) : NonUnitalNormedRing ↥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 = NonUnitalNormedRing.mk ⋯ ⋯

@[instance 75]

instance NonUnitalSubalgebraClass.nonUnitalNormedRing {S : Type u_5} {𝕜 : Type u_6} {E : Type u_7} [CommRing 𝕜] [NonUnitalNormedRing E] [Module 𝕜 E] [SetLike S E] [NonUnitalSubringClass S E] [SMulMemClass S 𝕜 E] (s : S) : NonUnitalNormedRing ↥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

• NonUnitalSubalgebraClass.nonUnitalNormedRing s = NonUnitalNormedRing.mk ⋯ ⋯

instance ULift.nonUnitalSeminormedRing {α : Type u_2} [NonUnitalSeminormedRing α] : NonUnitalSeminormedRing (ULift.{u_5, u_2} α)

Equations

• ULift.nonUnitalSeminormedRing = NonUnitalSeminormedRing.mk ⋯ ⋯

instance Prod.nonUnitalSeminormedRing {α : Type u_2} {β : Type u_3} [NonUnitalSeminormedRing α] [NonUnitalSeminormedRing β] : NonUnitalSeminormedRing (α × β)

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

Equations

• Prod.nonUnitalSeminormedRing = NonUnitalSeminormedRing.mk ⋯ ⋯

instance MulOpposite.instNonUnitalSeminormedRing {α : Type u_2} [NonUnitalSeminormedRing α] : NonUnitalSeminormedRing αᵐᵒᵖ

Equations

• MulOpposite.instNonUnitalSeminormedRing = NonUnitalSeminormedRing.mk ⋯ ⋯

instance Subalgebra.seminormedRing {𝕜 : Type u_5} [CommRing 𝕜] {E : Type u_6} [SeminormedRing E] [Algebra 𝕜 E] (s : Subalgebra 𝕜 E) : SeminormedRing ↥s

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

Equations

• s.seminormedRing = SeminormedRing.mk ⋯ ⋯

@[instance 75]

instance SubalgebraClass.seminormedRing {S : Type u_5} {𝕜 : Type u_6} {E : Type u_7} [CommRing 𝕜] [SeminormedRing E] [Algebra 𝕜 E] [SetLike S E] [SubringClass S E] [SMulMemClass S 𝕜 E] (s : S) : SeminormedRing ↥s

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

Equations

• SubalgebraClass.seminormedRing s = SeminormedRing.mk ⋯ ⋯

instance Subalgebra.normedRing {𝕜 : Type u_5} [CommRing 𝕜] {E : Type u_6} [NormedRing E] [Algebra 𝕜 E] (s : Subalgebra 𝕜 E) : NormedRing ↥s

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

Equations

• s.normedRing = NormedRing.mk ⋯ ⋯

@[instance 75]

instance SubalgebraClass.normedRing {S : Type u_5} {𝕜 : Type u_6} {E : Type u_7} [CommRing 𝕜] [NormedRing E] [Algebra 𝕜 E] [SetLike S E] [SubringClass S E] [SMulMemClass S 𝕜 E] (s : S) : NormedRing ↥s

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

Equations

• SubalgebraClass.normedRing s = NormedRing.mk ⋯ ⋯

theorem Nat.norm_cast_le {α : Type u_2} [SeminormedRing α] (n : ℕ) : ‖↑n‖ ≤ ↑n * ‖1‖

theorem List.norm_prod_le' {α : Type u_2} [SeminormedRing α] {l : List α} : l ≠ [] → ‖l.prod‖ ≤ (map norm l).prod

theorem List.nnnorm_prod_le' {α : Type u_2} [SeminormedRing α] {l : List α} (hl : l ≠ []) : ‖l.prod‖₊ ≤ (map nnnorm l).prod

theorem List.norm_prod_le {α : Type u_2} [SeminormedRing α] [NormOneClass α] (l : List α) : ‖l.prod‖ ≤ (map norm l).prod

theorem List.nnnorm_prod_le {α : Type u_2} [SeminormedRing α] [NormOneClass α] (l : List α) : ‖l.prod‖₊ ≤ (map nnnorm l).prod

theorem Finset.norm_prod_le' {ι : Type u_4} {α : Type u_5} [NormedCommRing α] (s : Finset ι) (hs : s.Nonempty) (f : ι → α) : ‖∏ i ∈ s, f i‖ ≤ ∏ i ∈ s, ‖f i‖

theorem Finset.nnnorm_prod_le' {ι : Type u_4} {α : Type u_5} [NormedCommRing α] (s : Finset ι) (hs : s.Nonempty) (f : ι → α) : ‖∏ i ∈ s, f i‖₊ ≤ ∏ i ∈ s, ‖f i‖₊

theorem Finset.norm_prod_le {ι : Type u_4} {α : Type u_5} [NormedCommRing α] [NormOneClass α] (s : Finset ι) (f : ι → α) : ‖∏ i ∈ s, f i‖ ≤ ∏ i ∈ s, ‖f i‖

theorem Finset.nnnorm_prod_le {ι : Type u_4} {α : Type u_5} [NormedCommRing α] [NormOneClass α] (s : Finset ι) (f : ι → α) : ‖∏ i ∈ s, f i‖₊ ≤ ∏ i ∈ s, ‖f i‖₊

theorem nnnorm_pow_le' {α : Type u_2} [SeminormedRing α] (a : α) {n : ℕ} : 0 < n → ‖a ^ 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_2} [SeminormedRing α] [NormOneClass α] (a : α) (n : ℕ) : ‖a ^ n‖₊ ≤ ‖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_2} [SeminormedRing α] (a : α) {n : ℕ} (h : 0 < n) : ‖a ^ n‖ ≤ ‖a‖ ^ 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_2} [SeminormedRing α] [NormOneClass α] (a : α) (n : ℕ) : ‖a ^ n‖ ≤ ‖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_2} [SeminormedRing α] (a : α) : ∀ᶠ (n : ℕ) in Filter.atTop, ‖a ^ n‖ ≤ ‖a‖ ^ n

instance ULift.seminormedRing {α : Type u_2} [SeminormedRing α] : SeminormedRing (ULift.{u_5, u_2} α)

Equations

• ULift.seminormedRing = SeminormedRing.mk ⋯ ⋯

instance Prod.seminormedRing {α : Type u_2} {β : Type u_3} [SeminormedRing α] [SeminormedRing β] : SeminormedRing (α × β)

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

Equations

• Prod.seminormedRing = SeminormedRing.mk ⋯ ⋯

instance MulOpposite.instSeminormedRing {α : Type u_2} [SeminormedRing α] : SeminormedRing αᵐᵒᵖ

Equations

• MulOpposite.instSeminormedRing = SeminormedRing.mk ⋯ ⋯

theorem norm_sub_mul_le {α : Type u_2} [SeminormedRing α] {a b c : α} (ha : ‖a‖ ≤ 1) : ‖c - a * b‖ ≤ ‖c - a‖ + ‖1 - b‖

This inequality is particularly useful when c = 1 and ‖a‖ = ‖b‖ = 1 as it then shows that chord length is a metric on the unit complex numbers.

theorem norm_sub_mul_le' {α : Type u_2} [SeminormedRing α] {a b c : α} (hb : ‖b‖ ≤ 1) : ‖c - a * b‖ ≤ ‖1 - a‖ + ‖c - b‖

This inequality is particularly useful when c = 1 and ‖a‖ = ‖b‖ = 1 as it then shows that chord length is a metric on the unit complex numbers.

theorem nnnorm_sub_mul_le {α : Type u_2} [SeminormedRing α] {a b c : α} (ha : ‖a‖₊ ≤ 1) : ‖c - a * b‖₊ ≤ ‖c - a‖₊ + ‖1 - b‖₊

This inequality is particularly useful when c = 1 and ‖a‖ = ‖b‖ = 1 as it then shows that chord length is a metric on the unit complex numbers.

theorem nnnorm_sub_mul_le' {α : Type u_2} [SeminormedRing α] {a b c : α} (hb : ‖b‖₊ ≤ 1) : ‖c - a * b‖₊ ≤ ‖1 - a‖₊ + ‖c - b‖₊

This inequality is particularly useful when c = 1 and ‖a‖ = ‖b‖ = 1 as it then shows that chord length is a metric on the unit complex numbers.

theorem norm_commutator_units_sub_one_le {α : Type u_2} [SeminormedRing α] (a b : αˣ) : ‖↑(a * b * a⁻¹ * b⁻¹) - 1‖ ≤ 2 * ‖↑a⁻¹‖ * ‖↑b⁻¹‖ * ‖↑a - 1‖ * ‖↑b - 1‖

theorem nnnorm_commutator_units_sub_one_le {α : Type u_2} [SeminormedRing α] (a b : αˣ) : ‖↑(a * b * a⁻¹ * b⁻¹) - 1‖₊ ≤ 2 * ‖↑a⁻¹‖₊ * ‖↑b⁻¹‖₊ * ‖↑a - 1‖₊ * ‖↑b - 1‖₊

def RingHom.IsBounded {α : Type u_5} [SeminormedRing α] {β : Type u_6} [SeminormedRing β] (f : α →+* β) : Prop

A homomorphism f between semi_normed_rings is bounded if there exists a positive constant C such that for all x in α, norm (f x) ≤ C * norm x.

Equations

• f.IsBounded = ∃ (C : ℝ), 0 < C ∧ ∀ (x : α), ‖f x‖ ≤ C * ‖x‖

instance ULift.nonUnitalNormedRing {α : Type u_2} [NonUnitalNormedRing α] : NonUnitalNormedRing (ULift.{u_5, u_2} α)

Equations

• ULift.nonUnitalNormedRing = NonUnitalNormedRing.mk ⋯ ⋯

instance Prod.nonUnitalNormedRing {α : Type u_2} {β : Type u_3} [NonUnitalNormedRing α] [NonUnitalNormedRing β] : NonUnitalNormedRing (α × β)

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

Equations

• Prod.nonUnitalNormedRing = NonUnitalNormedRing.mk ⋯ ⋯

instance MulOpposite.instNonUnitalNormedRing {α : Type u_2} [NonUnitalNormedRing α] : NonUnitalNormedRing αᵐᵒᵖ

Equations

• MulOpposite.instNonUnitalNormedRing = NonUnitalNormedRing.mk ⋯ ⋯

theorem Units.norm_pos {α : Type u_2} [NormedRing α] [Nontrivial α] (x : αˣ) : 0 < ‖↑x‖

theorem Units.nnnorm_pos {α : Type u_2} [NormedRing α] [Nontrivial α] (x : αˣ) : 0 < ‖↑x‖₊

instance ULift.normedRing {α : Type u_2} [NormedRing α] : NormedRing (ULift.{u_5, u_2} α)

Equations

• ULift.normedRing = NormedRing.mk ⋯ ⋯

instance Prod.normedRing {α : Type u_2} {β : Type u_3} [NormedRing α] [NormedRing β] : NormedRing (α × β)

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

Equations

• Prod.normedRing = NormedRing.mk ⋯ ⋯

instance MulOpposite.instNormedRing {α : Type u_2} [NormedRing α] : NormedRing αᵐᵒᵖ

Equations

• MulOpposite.instNormedRing = NormedRing.mk ⋯ ⋯

instance ULift.nonUnitalSeminormedCommRing {α : Type u_2} [NonUnitalSeminormedCommRing α] : NonUnitalSeminormedCommRing (ULift.{u_5, u_2} α)

Equations

• ULift.nonUnitalSeminormedCommRing = NonUnitalSeminormedCommRing.mk ⋯

instance Prod.nonUnitalSeminormedCommRing {α : Type u_2} {β : Type u_3} [NonUnitalSeminormedCommRing α] [NonUnitalSeminormedCommRing β] : NonUnitalSeminormedCommRing (α × β)

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

Equations

• Prod.nonUnitalSeminormedCommRing = NonUnitalSeminormedCommRing.mk ⋯

instance MulOpposite.instNonUnitalSeminormedCommRing {α : Type u_2} [NonUnitalSeminormedCommRing α] : NonUnitalSeminormedCommRing αᵐᵒᵖ

Equations

• MulOpposite.instNonUnitalSeminormedCommRing = NonUnitalSeminormedCommRing.mk ⋯

instance NonUnitalSubalgebra.nonUnitalSeminormedCommRing {𝕜 : Type u_5} [CommRing 𝕜] {E : Type u_6} [NonUnitalSeminormedCommRing E] [Module 𝕜 E] (s : NonUnitalSubalgebra 𝕜 E) : NonUnitalSeminormedCommRing ↥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 = NonUnitalSeminormedCommRing.mk ⋯

instance NonUnitalSubalgebra.nonUnitalNormedCommRing {𝕜 : Type u_5} [CommRing 𝕜] {E : Type u_6} [NonUnitalNormedCommRing E] [Module 𝕜 E] (s : NonUnitalSubalgebra 𝕜 E) : NonUnitalNormedCommRing ↥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 = NonUnitalNormedCommRing.mk ⋯

instance ULift.nonUnitalNormedCommRing {α : Type u_2} [NonUnitalNormedCommRing α] : NonUnitalNormedCommRing (ULift.{u_5, u_2} α)

Equations

• ULift.nonUnitalNormedCommRing = NonUnitalNormedCommRing.mk ⋯

instance Prod.nonUnitalNormedCommRing {α : Type u_2} {β : Type u_3} [NonUnitalNormedCommRing α] [NonUnitalNormedCommRing β] : NonUnitalNormedCommRing (α × β)

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

Equations

• Prod.nonUnitalNormedCommRing = NonUnitalNormedCommRing.mk ⋯

instance MulOpposite.instNonUnitalNormedCommRing {α : Type u_2} [NonUnitalNormedCommRing α] : NonUnitalNormedCommRing αᵐᵒᵖ

Equations

• MulOpposite.instNonUnitalNormedCommRing = NonUnitalNormedCommRing.mk ⋯

instance ULift.seminormedCommRing {α : Type u_2} [SeminormedCommRing α] : SeminormedCommRing (ULift.{u_5, u_2} α)

Equations

• ULift.seminormedCommRing = SeminormedCommRing.mk ⋯

instance Prod.seminormedCommRing {α : Type u_2} {β : Type u_3} [SeminormedCommRing α] [SeminormedCommRing β] : SeminormedCommRing (α × β)

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

Equations

• Prod.seminormedCommRing = SeminormedCommRing.mk ⋯

instance MulOpposite.instSeminormedCommRing {α : Type u_2} [SeminormedCommRing α] : SeminormedCommRing αᵐᵒᵖ

Equations

• MulOpposite.instSeminormedCommRing = SeminormedCommRing.mk ⋯

instance Subalgebra.seminormedCommRing {𝕜 : Type u_5} [CommRing 𝕜] {E : Type u_6} [SeminormedCommRing E] [Algebra 𝕜 E] (s : Subalgebra 𝕜 E) : SeminormedCommRing ↥s

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

Equations

• s.seminormedCommRing = SeminormedCommRing.mk ⋯

instance Subalgebra.normedCommRing {𝕜 : Type u_5} [CommRing 𝕜] {E : Type u_6} [NormedCommRing E] [Algebra 𝕜 E] (s : Subalgebra 𝕜 E) : NormedCommRing ↥s

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

Equations

• s.normedCommRing = NormedCommRing.mk ⋯

instance ULift.normedCommRing {α : Type u_2} [NormedCommRing α] : NormedCommRing (ULift.{u_5, u_2} α)

Equations

• ULift.normedCommRing = NormedCommRing.mk ⋯

instance Prod.normedCommRing {α : Type u_2} {β : Type u_3} [NormedCommRing α] [NormedCommRing β] : NormedCommRing (α × β)

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

Equations

• Prod.normedCommRing = NormedCommRing.mk ⋯

instance MulOpposite.instNormedCommRing {α : Type u_2} [NormedCommRing α] : NormedCommRing αᵐᵒᵖ

Equations

• MulOpposite.instNormedCommRing = NormedCommRing.mk ⋯

theorem IsPowMul.restriction {R : Type u_5} {S : Type u_6} [CommRing R] [Ring S] [Algebra R S] (A : Subalgebra R S) {f : S → ℝ} (hf_pm : IsPowMul f) : IsPowMul fun (x : ↥A) => f ↑x

The restriction of a power-multiplicative function to a subalgebra is power-multiplicative.

instance Real.normedCommRing : NormedCommRing ℝ

Equations

• Real.normedCommRing = NormedCommRing.mk ⋯

theorem NNReal.norm_eq (x : NNReal) : ‖↑x‖ = ↑x

@[simp]

theorem NNReal.nnnorm_eq (x : NNReal) : ‖↑x‖₊ = x

@[simp]

theorem NNReal.enorm_eq (x : NNReal) : ‖↑x‖ₑ = ↑x

theorem NormedAddCommGroup.tendsto_atTop {α : Type u_2} [Nonempty α] [Preorder α] [IsDirected α fun (x1 x2 : α) => x1 ≤ x2] {β : Type u_5} [SeminormedAddCommGroup β] {f : α → β} {b : β} : Filter.Tendsto f Filter.atTop (nhds b) ↔ ∀ (ε : ℝ), 0 < ε → ∃ (N : α), ∀ (n : α), N ≤ n → ‖f n - b‖ < ε

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

theorem NormedAddCommGroup.tendsto_atTop' {α : Type u_2} [Nonempty α] [Preorder α] [IsDirected α fun (x1 x2 : α) => x1 ≤ x2] [NoMaxOrder α] {β : Type u_5} [SeminormedAddCommGroup β] {f : α → β} {b : β} : Filter.Tendsto f Filter.atTop (nhds b) ↔ ∀ (ε : ℝ), 0 < ε → ∃ (N : α), ∀ (n : α), N < n → ‖f n - b‖ < ε

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

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

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

• RingHomIsometric.ids
• RingHomIsometric.starRingEnd

instance RingHomIsometric.ids {R₁ : Type u_5} [SeminormedRing R₁] : RingHomIsometric (RingHom.id R₁)

class NormMulClass (α : Type u_5) [Norm α] [Mul α] : Prop

A mixin class for strict multiplicativity of the norm, ‖a * b‖ = ‖a‖ * ‖b‖ (rather than ≤ as in the definition of NormedRing). Many NormedRings satisfy this stronger property, including all NormedDivisionRings and NormedFields.

• norm_mul (a b : α) : ‖a * b‖ = ‖a‖ * ‖b‖

  The norm is multiplicative.

Instances

• Int.instNormMulClass
• NormedDivisionRing.toNormMulClass
• PadicInt.instNormMulClass
• SubringClass.toNormMulClass

@[simp]

theorem norm_mul {α : Type u_2} [Norm α] [Mul α] [NormMulClass α] (a b : α) : ‖a * b‖ = ‖a‖ * ‖b‖

@[simp]

theorem nnnorm_mul {α : Type u_2} [SeminormedAddCommGroup α] [Mul α] [NormMulClass α] (a b : α) : ‖a * b‖₊ = ‖a‖₊ * ‖b‖₊

@[simp]

theorem enorm_mul {α : Type u_2} [SeminormedAddCommGroup α] [Mul α] [NormMulClass α] (a b : α) : ‖a * b‖ₑ = ‖a‖ₑ * ‖b‖ₑ

def normHom {α : Type u_2} [SeminormedRing α] [NormOneClass α] [NormMulClass α] : α →*₀ ℝ

norm as a MonoidWithZeroHom.

Equations

• normHom = { toFun := fun (x : α) => ‖x‖, map_zero' := ⋯, map_one' := ⋯, map_mul' := ⋯ }

@[simp]

theorem normHom_apply {α : Type u_2} [SeminormedRing α] [NormOneClass α] [NormMulClass α] (x✝ : α) : normHom x✝ = ‖x✝‖

def nnnormHom {α : Type u_2} [SeminormedRing α] [NormOneClass α] [NormMulClass α] : α →*₀ NNReal

nnnorm as a MonoidWithZeroHom.

Equations

• nnnormHom = { toFun := fun (x : α) => ‖x‖₊, map_zero' := ⋯, map_one' := ⋯, map_mul' := ⋯ }

@[simp]

theorem nnnormHom_apply {α : Type u_2} [SeminormedRing α] [NormOneClass α] [NormMulClass α] (x✝ : α) : nnnormHom x✝ = ‖x✝‖₊

@[simp]

theorem norm_pow {α : Type u_2} [SeminormedRing α] [NormOneClass α] [NormMulClass α] (a : α) (n : ℕ) : ‖a ^ n‖ = ‖a‖ ^ n

@[simp]

theorem nnnorm_pow {α : Type u_2} [SeminormedRing α] [NormOneClass α] [NormMulClass α] (a : α) (n : ℕ) : ‖a ^ n‖₊ = ‖a‖₊ ^ n

@[simp]

theorem enorm_pow {α : Type u_2} [SeminormedRing α] [NormOneClass α] [NormMulClass α] (a : α) (n : ℕ) : ‖a ^ n‖ₑ = ‖a‖ₑ ^ n

theorem List.norm_prod {α : Type u_2} [SeminormedRing α] [NormOneClass α] [NormMulClass α] (l : List α) : ‖l.prod‖ = (map norm l).prod

theorem List.nnnorm_prod {α : Type u_2} [SeminormedRing α] [NormOneClass α] [NormMulClass α] (l : List α) : ‖l.prod‖₊ = (map nnnorm l).prod

@[simp]

theorem norm_prod {α : Type u_2} {β : Type u_3} [SeminormedCommRing α] [NormMulClass α] [NormOneClass α] (s : Finset β) (f : β → α) : ‖∏ b ∈ s, f b‖ = ∏ b ∈ s, ‖f b‖

@[simp]

theorem nnnorm_prod {α : Type u_2} {β : Type u_3} [SeminormedCommRing α] [NormMulClass α] [NormOneClass α] (s : Finset β) (f : β → α) : ‖∏ b ∈ s, f b‖₊ = ∏ b ∈ s, ‖f b‖₊

theorem NormMulClass.toNormOneClass {α : Type u_2} [NormedAddCommGroup α] [MulOneClass α] [NormMulClass α] [Nontrivial α] : NormOneClass α

Deduce NormOneClass from NormMulClass under a suitable nontriviality hypothesis. Not an instance, in order to avoid loops with NormOneClass.nontrivial.

instance NormMulClass.isAbsoluteValue_norm {α : Type u_2} [NormedRing α] [NormMulClass α] : IsAbsoluteValue norm

instance NormMulClass.toNoZeroDivisors {α : Type u_2} [NormedRing α] [NormMulClass α] : NoZeroDivisors α

Induced normed structures

@[reducible, inline]

abbrev NonUnitalSeminormedRing.induced {F : Type u_5} (R : Type u_6) (S : Type u_7) [FunLike F R S] [NonUnitalRing R] [NonUnitalSeminormedRing S] [NonUnitalRingHomClass F R S] (f : F) : NonUnitalSeminormedRing R

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

See note [reducible non-instances]

Equations

• NonUnitalSeminormedRing.induced R S f = NonUnitalSeminormedRing.mk ⋯ ⋯

@[reducible, inline]

abbrev NonUnitalNormedRing.induced {F : Type u_5} (R : Type u_6) (S : Type u_7) [FunLike F R S] [NonUnitalRing R] [NonUnitalNormedRing S] [NonUnitalRingHomClass F R S] (f : F) (hf : Function.Injective ⇑f) : NonUnitalNormedRing R

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

• NonUnitalNormedRing.induced R S f hf = NonUnitalNormedRing.mk ⋯ ⋯

@[reducible, inline]

abbrev SeminormedRing.induced {F : Type u_5} (R : Type u_6) (S : Type u_7) [FunLike F R S] [Ring R] [SeminormedRing S] [NonUnitalRingHomClass F R S] (f : F) : SeminormedRing R

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

See note [reducible non-instances]

Equations

• SeminormedRing.induced R S f = SeminormedRing.mk ⋯ ⋯

@[reducible, inline]

abbrev NormedRing.induced {F : Type u_5} (R : Type u_6) (S : Type u_7) [FunLike F R S] [Ring R] [NormedRing S] [NonUnitalRingHomClass F R S] (f : F) (hf : Function.Injective ⇑f) : NormedRing R

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

• NormedRing.induced R S f hf = NormedRing.mk ⋯ ⋯

@[reducible, inline]

abbrev NonUnitalSeminormedCommRing.induced {F : Type u_5} (R : Type u_6) (S : Type u_7) [FunLike F R S] [NonUnitalCommRing R] [NonUnitalSeminormedCommRing S] [NonUnitalRingHomClass F R S] (f : F) : NonUnitalSeminormedCommRing R

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

See note [reducible non-instances]

Equations

• NonUnitalSeminormedCommRing.induced R S f = NonUnitalSeminormedCommRing.mk ⋯

@[reducible, inline]

abbrev NonUnitalNormedCommRing.induced {F : Type u_5} (R : Type u_6) (S : Type u_7) [FunLike F R S] [NonUnitalCommRing R] [NonUnitalNormedCommRing S] [NonUnitalRingHomClass F R S] (f : F) (hf : Function.Injective ⇑f) : NonUnitalNormedCommRing R

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

• NonUnitalNormedCommRing.induced R S f hf = NonUnitalNormedCommRing.mk ⋯

@[reducible, inline]

abbrev SeminormedCommRing.induced {F : Type u_5} (R : Type u_6) (S : Type u_7) [FunLike F R S] [CommRing R] [SeminormedRing S] [NonUnitalRingHomClass F R S] (f : F) : SeminormedCommRing R

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

See note [reducible non-instances]

Equations

• SeminormedCommRing.induced R S f = SeminormedCommRing.mk ⋯

@[reducible, inline]

abbrev NormedCommRing.induced {F : Type u_5} (R : Type u_6) (S : Type u_7) [FunLike F R S] [CommRing R] [NormedRing S] [NonUnitalRingHomClass F R S] (f : F) (hf : Function.Injective ⇑f) : NormedCommRing R

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

• NormedCommRing.induced R S f hf = NormedCommRing.mk ⋯

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

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.

theorem NormMulClass.induced {F : Type u_8} (R : Type u_9) (S : Type u_10) [Ring R] [SeminormedRing S] [NormMulClass S] [FunLike F R S] [RingHomClass F R S] (f : F) : NormMulClass R

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] [SeminormedRing R] [SubringClass S R] (s : S) : SeminormedRing ↥s

Equations

• SubringClass.toSeminormedRing s = SeminormedRing.induced (↥s) R (SubringClass.subtype s)

instance SubringClass.toNormedRing {S : Type u_5} {R : Type u_6} [SetLike S R] [NormedRing R] [SubringClass S R] (s : S) : NormedRing ↥s

Equations

• SubringClass.toNormedRing s = NormedRing.induced (↥s) R (SubringClass.subtype s) ⋯

instance SubringClass.toSeminormedCommRing {S : Type u_5} {R : Type u_6} [SetLike S R] [SeminormedCommRing R] [_h : SubringClass S R] (s : S) : SeminormedCommRing ↥s

Equations

• SubringClass.toSeminormedCommRing s = SeminormedCommRing.mk ⋯

instance SubringClass.toNormedCommRing {S : Type u_5} {R : Type u_6} [SetLike S R] [NormedCommRing R] [SubringClass S R] (s : S) : NormedCommRing ↥s

Equations

• SubringClass.toNormedCommRing s = NormedCommRing.mk ⋯

instance SubringClass.toNormOneClass {S : Type u_5} {R : Type u_6} [SetLike S R] [SeminormedRing R] [NormOneClass R] [SubringClass S R] (s : S) : NormOneClass ↥s

instance SubringClass.toNormMulClass {S : Type u_5} {R : Type u_6} [SetLike S R] [SeminormedRing R] [NormMulClass R] [SubringClass S R] (s : S) : NormMulClass ↥s

noncomputable def AbsoluteValue.toNormedRing {R : Type u_5} [Ring R] (v : AbsoluteValue R ℝ) : NormedRing R

A real absolute value on a ring determines a NormedRing structure.

Equations

• v.toNormedRing = NormedRing.mk ⋯ ⋯