# 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`.

source
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

source
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 : ↑0 = 0
- natCast_succ (n : ℕ) : ↑(n + 1) = ↑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

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

A seminormed ring is a non-unital seminormed ring.

Equations

- One or more equations did not get rendered due to their size.

source
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

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

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

Equations

- NonUnitalNormedRing.toNonUnitalSeminormedRing = { toNorm := β.toNorm, toNonUnitalRing := β.toNonUnitalRing, toPseudoMetricSpace := β.toPseudoMetricSpace, dist_eq := ⋯, norm_mul_le := ⋯ }

source
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 : ↑0 = 0
- natCast_succ (n : ℕ) : ↑(n + 1) = ↑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

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

A normed ring is a seminormed ring.

Equations

- NormedRing.toSeminormedRing = { toNorm := β.toNorm, toRing := β.toRing, toPseudoMetricSpace := β.toPseudoMetricSpace, dist_eq := ⋯, norm_mul_le := ⋯ }

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

A normed ring is a non-unital normed ring.

Equations

- One or more equations did not get rendered due to their size.

source
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

source
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

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

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

Equations

- One or more equations did not get rendered due to their size.

source
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 : ↑0 = 0
- natCast_succ (n : ℕ) : ↑(n + 1) = ↑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

source
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 : ↑0 = 0
- natCast_succ (n : ℕ) : ↑(n + 1) = ↑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

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

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

Equations

- One or more equations did not get rendered due to their size.

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

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

Equations

- One or more equations did not get rendered due to their size.

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

A normed commutative ring is a seminormed commutative ring.

Equations

- NormedCommRing.toSeminormedCommRing = { toNorm := β.toNorm, toRing := β.toRing, toPseudoMetricSpace := β.toPseudoMetricSpace, dist_eq := ⋯, norm_mul_le := ⋯, mul_comm := ⋯ }

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

- One or more equations did not get rendered due to their size.

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

A mixin class with the axiom `‖1‖ = 1`. Many `NormedRing`s and all `NormedField`s satisfy this axiom.

- norm_one : ‖1‖ = 1

  The norm of the multiplicative identity is 1.

Instances

source
@[simp]
theorem nnnorm_one {G : Type u_1} [SeminormedAddCommGroup G] [One G] [NormOneClass G] :
‖1‖₊ = 1
source
@[simp]
theorem enorm_one {G : Type u_1} [SeminormedAddCommGroup G] [One G] [NormOneClass G] :
‖1‖ₑ = 1
source
theorem NormOneClass.nontrivial {G : Type u_1} [SeminormedAddCommGroup G] [One G] [NormOneClass G] :
Nontrivial G
source
@[instance 100]
instance NonUnitalNormedRing.toNormedAddCommGroup {α : Type u_2} [β : NonUnitalNormedRing α] :
NormedAddCommGroup α
Equations

- NonUnitalNormedRing.toNormedAddCommGroup = { toNorm := β.toNorm, toAddCommGroup := β.toAddCommGroup, toMetricSpace := β.toMetricSpace, dist_eq := ⋯ }

source
@[instance 100]
instance NonUnitalSeminormedRing.toSeminormedAddCommGroup {α : Type u_2} [NonUnitalSeminormedRing α] :
SeminormedAddCommGroup α
Equations

- NonUnitalSeminormedRing.toSeminormedAddCommGroup = { toNorm := inst✝.toNorm, toAddCommGroup := inst✝.toAddCommGroup, toPseudoMetricSpace := inst✝.toPseudoMetricSpace, dist_eq := ⋯ }

source
instance ULift.normOneClass {α : Type u_2} [SeminormedAddCommGroup α] [One α] [NormOneClass α] :
NormOneClass (ULift.{u_5, u_2} α)
source
instance Prod.normOneClass {α : Type u_2} {β : Type u_3} [SeminormedAddCommGroup α] [One α] [NormOneClass α] [SeminormedAddCommGroup β] [One β] [NormOneClass β] :
NormOneClass (α × β)
source
instance Pi.normOneClass {ι : Type u_5} {α : ι → Type u_6} [Nonempty ι] [Fintype ι] [(i : ι) → SeminormedAddCommGroup (α i)] [(i : ι) → One (α i)] [∀ (i : ι), NormOneClass (α i)] :
NormOneClass ((i : ι) → α i)
source
instance MulOpposite.normOneClass {α : Type u_2} [SeminormedAddCommGroup α] [One α] [NormOneClass α] :
NormOneClass α ᵐᵒᵖ
source
theorem norm_mul_le {α : Type u_2} [NonUnitalSeminormedRing α] (a b : α) :
‖a * b‖ ≤ ‖a‖ * ‖b‖

The norm is submultiplicative.

source
theorem nnnorm_mul_le {α : Type u_2} [NonUnitalSeminormedRing α] (a b : α) :
‖a * b‖₊ ≤ ‖a‖₊ * ‖b‖₊
source
theorem norm_mul_le_of_le {α : Type u_2} [NonUnitalSeminormedRing α] {a₁ a₂ : α} {r₁ r₂ : ℝ} (h₁ : ‖a₁‖ ≤ r₁) (h₂ : ‖a₂‖ ≤ r₂) :
‖a₁ * a₂‖ ≤ r₁ * r₂
source
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₂
source
theorem norm_mul₃_le {α : Type u_2} [NonUnitalSeminormedRing α] {a b c : α} :
‖a * b * c‖ ≤ ‖a‖ * ‖b‖ * ‖c‖
source
theorem nnnorm_mul₃_le {α : Type u_2} [NonUnitalSeminormedRing α] {a b c : α} :
‖a * b * c‖₊ ≤ ‖a‖₊ * ‖b‖₊ * ‖c‖₊
source
theorem one_le_norm_one (β : Type u_5) [NormedRing β] [Nontrivial β] :
1 ≤ ‖1‖
source
theorem one_le_nnnorm_one (β : Type u_5) [NormedRing β] [Nontrivial β] :
1 ≤ ‖1‖₊
source
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.

source
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.

source
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

- One or more equations did not get rendered due to their size.

source
@[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

- One or more equations did not get rendered due to their size.

source
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

- One or more equations did not get rendered due to their size.

source
@[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

- One or more equations did not get rendered due to their size.

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

- One or more equations did not get rendered due to their size.

source
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

- One or more equations did not get rendered due to their size.

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

- One or more equations did not get rendered due to their size.

source
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

- One or more equations did not get rendered due to their size.

source
@[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

- One or more equations did not get rendered due to their size.

source
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

- One or more equations did not get rendered due to their size.

source
@[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

- One or more equations did not get rendered due to their size.

source
theorem Nat.norm_cast_le {α : Type u_2} [SeminormedRing α] (n : ℕ) :
‖↑n‖ ≤ ↑n * ‖1‖
source
theorem List.norm_prod_le' {α : Type u_2} [SeminormedRing α] {l : List α} :
l ≠ [] → ‖l.prod‖ ≤ (map norm l).prod
source
theorem List.nnnorm_prod_le' {α : Type u_2} [SeminormedRing α] {l : List α} (hl : l ≠ []) :
‖l.prod‖₊ ≤ (map nnnorm l).prod
source
theorem List.norm_prod_le {α : Type u_2} [SeminormedRing α] [NormOneClass α] (l : List α) :
‖l.prod‖ ≤ (map norm l).prod
source
theorem List.nnnorm_prod_le {α : Type u_2} [SeminormedRing α] [NormOneClass α] (l : List α) :
‖l.prod‖₊ ≤ (map nnnorm l).prod
source
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‖
source
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‖₊
source
theorem Finset.norm_prod_le {ι : Type u_4} {α : Type u_5} [NormedCommRing α] [NormOneClass α] (s : Finset ι) (f : ι → α) :
‖∏ i ∈ s, f i‖ ≤ ∏ i ∈ s, ‖f i‖
source
theorem Finset.nnnorm_prod_le {ι : Type u_4} {α : Type u_5} [NormedCommRing α] [NormOneClass α] (s : Finset ι) (f : ι → α) :
‖∏ i ∈ s, f i‖₊ ≤ ∏ i ∈ s, ‖f i‖₊
source
theorem norm_natAbs {α : Type u_2} [SeminormedRing α] (z : ℤ) :
‖↑z.natAbs‖ = ‖↑z‖
source
theorem nnnorm_natAbs {α : Type u_2} [SeminormedRing α] (z : ℤ) :
‖↑z.natAbs‖₊ = ‖↑z‖₊
source
@[simp]
theorem norm_intCast_abs {α : Type u_2} [SeminormedRing α] (z : ℤ) :
‖↑|z|‖ = ‖↑z‖
source
@[simp]
theorem nnnorm_intCast_abs {α : Type u_2} [SeminormedRing α] (z : ℤ) :
‖↑|z|‖₊ = ‖↑z‖₊
source
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`.

source
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'`.

source
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`.

source
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'`.

source
theorem eventually_norm_pow_le {α : Type u_2} [SeminormedRing α] (a : α) :
∀ᶠ (n : ℕ) in Filter.atTop, ‖a ^ n‖ ≤ ‖a‖ ^ n
source
instance ULift.seminormedRing {α : Type u_2} [SeminormedRing α] :
SeminormedRing (ULift.{u_5, u_2} α)
Equations

- One or more equations did not get rendered due to their size.

source
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

- One or more equations did not get rendered due to their size.

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

- One or more equations did not get rendered due to their size.

source
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.

source
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.

source
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.

source
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.

source
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‖
source
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‖₊
source
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‖

Instances For

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

- One or more equations did not get rendered due to their size.

source
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

- One or more equations did not get rendered due to their size.

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

- One or more equations did not get rendered due to their size.

source
theorem Units.norm_pos {α : Type u_2} [NormedRing α] [Nontrivial α] (x : α ˣ) :
0 < ‖↑x‖
source
theorem Units.nnnorm_pos {α : Type u_2} [NormedRing α] [Nontrivial α] (x : α ˣ) :
0 < ‖↑x‖₊
source
instance ULift.normedRing {α : Type u_2} [NormedRing α] :
NormedRing (ULift.{u_5, u_2} α)
Equations

- One or more equations did not get rendered due to their size.

source
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

- One or more equations did not get rendered due to their size.

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

- One or more equations did not get rendered due to their size.

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

- ULift.nonUnitalSeminormedCommRing = { toNonUnitalSeminormedRing := ULift.nonUnitalSeminormedRing, mul_comm := ⋯ }

source
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 = { toNonUnitalSeminormedRing := Prod.nonUnitalSeminormedRing, mul_comm := ⋯ }

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

- MulOpposite.instNonUnitalSeminormedCommRing = { toNonUnitalSeminormedRing := MulOpposite.instNonUnitalSeminormedRing, mul_comm := ⋯ }

source
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 = { toNonUnitalSeminormedRing := s.nonUnitalSeminormedRing, mul_comm := ⋯ }

source
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

- One or more equations did not get rendered due to their size.

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

- One or more equations did not get rendered due to their size.

source
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

- One or more equations did not get rendered due to their size.

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

- MulOpposite.instNonUnitalNormedCommRing = { toNonUnitalNormedRing := MulOpposite.instNonUnitalNormedRing, mul_comm := ⋯ }

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

- One or more equations did not get rendered due to their size.

source
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

- One or more equations did not get rendered due to their size.

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

- MulOpposite.instSeminormedCommRing = { toSeminormedRing := MulOpposite.instSeminormedRing, mul_comm := ⋯ }

source
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 = { toSeminormedRing := s.seminormedRing, mul_comm := ⋯ }

source
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

- One or more equations did not get rendered due to their size.

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

- ULift.normedCommRing = { toNormedRing := ULift.normedRing, mul_comm := ⋯ }

source
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

- One or more equations did not get rendered due to their size.

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

- MulOpposite.instNormedCommRing = { toNormedRing := MulOpposite.instNormedRing, mul_comm := ⋯ }

source
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.

source
instance Real.normedCommRing :
NormedCommRing ℝ
Equations

- One or more equations did not get rendered due to their size.

source
theorem NNReal.norm_eq (x : NNReal) :
‖↑x‖ = ↑x
source
@[simp]
theorem NNReal.nnnorm_eq (x : NNReal) :
‖↑x‖₊ = x
source
@[simp]
theorem NNReal.enorm_eq (x : NNReal) :
‖↑x‖ₑ = ↑x
source
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.

source
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, ...`

source
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.

- norm_map {x : R₁} : ‖σ x‖ = ‖x‖

  The ring homomorphism is an isometry.

Instances

source
@[deprecated RingHomIsometric.norm_map (since := "2025-08-03")]
theorem RingHomIsometric.is_iso {R₁ : Type u_5} {R₂ : Type u_6} {inst✝ : Semiring R₁} {inst✝¹ : Semiring R₂} {inst✝² : Norm R₁} {inst✝³ : Norm R₂} {σ : R₁ →+* R₂} [self : RingHomIsometric σ] {x : R₁} :
‖σ x‖ = ‖x‖

Alias of `RingHomIsometric.norm_map`.

The ring homomorphism is an isometry.

source
@[simp]
theorem RingHomIsometric.nnnorm_map {R₁ : Type u_5} {R₂ : Type u_6} [SeminormedRing R₁] [SeminormedRing R₂] (σ : R₁ →+* R₂) [RingHomIsometric σ] (x : R₁) :
‖σ x‖₊ = ‖x‖₊
source
@[simp]
theorem RingHomIsometric.enorm_map {R₁ : Type u_5} {R₂ : Type u_6} [SeminormedRing R₁] [SeminormedRing R₂] (σ : R₁ →+* R₂) [RingHomIsometric σ] (x : R₁) :
‖σ x‖ₑ = ‖x‖ₑ
source
instance RingHomIsometric.ids {R₁ : Type u_5} [SeminormedRing R₁] :
RingHomIsometric (RingHom.id R₁)
source
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 `NormedRing`s satisfy this stronger property, including all `NormedDivisionRing`s and `NormedField`s.

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

  The norm is multiplicative.

Instances

source
@[simp]
theorem norm_mul {α : Type u_2} [Norm α] [Mul α] [NormMulClass α] (a b : α) :
‖a * b‖ = ‖a‖ * ‖b‖
source
@[simp]
theorem nnnorm_mul {α : Type u_2} [SeminormedAddCommGroup α] [Mul α] [NormMulClass α] (a b : α) :
‖a * b‖₊ = ‖a‖₊ * ‖b‖₊
source
@[simp]
theorem enorm_mul {α : Type u_2} [SeminormedAddCommGroup α] [Mul α] [NormMulClass α] (a b : α) :
‖a * b‖ₑ = ‖a‖ₑ * ‖b‖ₑ
source
def normHom {α : Type u_2} [SeminormedRing α] [NormOneClass α] [NormMulClass α] :
α →*₀ ℝ

`norm` as a `MonoidWithZeroHom`.

Equations

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

Instances For

source
@[simp]
theorem normHom_apply {α : Type u_2} [SeminormedRing α] [NormOneClass α] [NormMulClass α] (x✝ : α) :
normHom x✝ = ‖x✝‖
source
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' := ⋯ }

Instances For

source
@[simp]
theorem nnnormHom_apply {α : Type u_2} [SeminormedRing α] [NormOneClass α] [NormMulClass α] (x✝ : α) :
nnnormHom x✝ = ‖x✝‖₊
source
@[simp]
theorem norm_pow {α : Type u_2} [SeminormedRing α] [NormOneClass α] [NormMulClass α] (a : α) (n : ℕ) :
‖a ^ n‖ = ‖a‖ ^ n
source
@[simp]
theorem nnnorm_pow {α : Type u_2} [SeminormedRing α] [NormOneClass α] [NormMulClass α] (a : α) (n : ℕ) :
‖a ^ n‖₊ = ‖a‖₊ ^ n
source
@[simp]
theorem enorm_pow {α : Type u_2} [SeminormedRing α] [NormOneClass α] [NormMulClass α] (a : α) (n : ℕ) :
‖a ^ n‖ₑ = ‖a‖ₑ ^ n
source
theorem List.norm_prod {α : Type u_2} [SeminormedRing α] [NormOneClass α] [NormMulClass α] (l : List α) :
‖l.prod‖ = (map norm l).prod
source
theorem List.nnnorm_prod {α : Type u_2} [SeminormedRing α] [NormOneClass α] [NormMulClass α] (l : List α) :
‖l.prod‖₊ = (map nnnorm l).prod
source
@[simp]
theorem norm_prod {α : Type u_2} {β : Type u_3} [SeminormedCommRing α] [NormMulClass α] [NormOneClass α] (s : Finset β) (f : β → α) :
‖∏ b ∈ s, f b‖ = ∏ b ∈ s, ‖f b‖
source
@[simp]
theorem nnnorm_prod {α : Type u_2} {β : Type u_3} [SeminormedCommRing α] [NormMulClass α] [NormOneClass α] (s : Finset β) (f : β → α) :
‖∏ b ∈ s, f b‖₊ = ∏ b ∈ s, ‖f b‖₊
source
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`.

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

### Induced normed structures #

source
@[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

- One or more equations did not get rendered due to their size.

Instances For

source
@[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

- One or more equations did not get rendered due to their size.

Instances For

source
@[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

- One or more equations did not get rendered due to their size.

Instances For

source
@[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

- One or more equations did not get rendered due to their size.

Instances For

source
@[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 = { toNonUnitalSeminormedRing := NonUnitalSeminormedRing.induced R S f, mul_comm := ⋯ }

Instances For

source
@[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 = { toNonUnitalNormedRing := NonUnitalNormedRing.induced R S f hf, mul_comm := ⋯ }

Instances For

source
@[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

- One or more equations did not get rendered due to their size.

Instances For

source
@[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

- One or more equations did not get rendered due to their size.

Instances For

source
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`.

source
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`.

source
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)

source
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) ⋯

source
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 = { toSeminormedRing := SubringClass.toSeminormedRing s, mul_comm := ⋯ }

source
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 = { toNormedRing := SubringClass.toNormedRing s, mul_comm := ⋯ }

source
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
source
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
source
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

- One or more equations did not get rendered due to their size.

Instances For