Normed fields

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

Some useful results that relate the topology of the normed field to the discrete topology include:

• norm_eq_one_iff_ne_zero_of_discrete

Methods for constructing a normed ring/field instance from a given real absolute value on a ring/field are given in:

• AbsoluteValue.toNormedRing
• AbsoluteValue.toNormedField

class NonUnitalSeminormedRing (α : Type u_4) extends Norm α, NonUnitalRing α, PseudoMetricSpace α : Type u_4

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 : α), PseudoMetricSpace.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 : ∀ (a b : α), ‖a * b‖ ≤ ‖a‖ * ‖b‖

  The norm is submultiplicative.

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

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 : α), PseudoMetricSpace.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 : ∀ (a b : α), ‖a * b‖ ≤ ‖a‖ * ‖b‖

  The norm is submultiplicative.

@[instance 100]

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

A seminormed ring is a non-unital seminormed ring.

Equations

• SeminormedRing.toNonUnitalSeminormedRing = NonUnitalSeminormedRing.mk ⋯ ⋯

class NonUnitalNormedRing (α : Type u_4) extends Norm α, NonUnitalRing α, MetricSpace α : Type u_4

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 : α), PseudoMetricSpace.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 : ∀ (a b : α), ‖a * b‖ ≤ ‖a‖ * ‖b‖

  The norm is submultiplicative.

@[instance 100]

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

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

Equations

• NonUnitalNormedRing.toNonUnitalSeminormedRing = NonUnitalSeminormedRing.mk ⋯ ⋯

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

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 : α), PseudoMetricSpace.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 : ∀ (a b : α), ‖a * b‖ ≤ ‖a‖ * ‖b‖

  The norm is submultiplicative.

class NormedDivisionRing (α : Type u_4) extends Norm α, DivisionRing α, MetricSpace α : Type u_4

A normed division ring is a division ring endowed with a seminorm which satisfies the equality ‖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)
• inv : α → α
• div : α → α → α
• div_eq_mul_inv : ∀ (a b : α), a / b = a * b⁻¹
• zpow : ℤ → α → α
• zpow_zero' : ∀ (a : α), DivisionRing.zpow 0 a = 1
• zpow_succ' : ∀ (n : ℕ) (a : α), DivisionRing.zpow (↑n.succ) a = DivisionRing.zpow (↑n) a * a
• zpow_neg' : ∀ (n : ℕ) (a : α), DivisionRing.zpow (Int.negSucc n) a = (DivisionRing.zpow (↑n.succ) a)⁻¹
• exists_pair_ne : ∃ (x : α) (y : α), x ≠ y
• nnratCast : ℚ≥0 → α
• ratCast : ℚ → α
• mul_inv_cancel : ∀ (a : α), a ≠ 0 → a * a⁻¹ = 1
• inv_zero : 0⁻¹ = 0
• nnratCast_def : ∀ (q : ℚ≥0), ↑q = ↑q.num / ↑q.den
• nnqsmul : ℚ≥0 → α → α
• nnqsmul_def : ∀ (q : ℚ≥0) (a : α), DivisionRing.nnqsmul q a = ↑q * a
• ratCast_def : ∀ (q : ℚ), ↑q = ↑q.num / ↑q.den
• qsmul : ℚ → α → α
• qsmul_def : ∀ (a : ℚ) (x : α), DivisionRing.qsmul a x = ↑a * x
• dist : α → α → ℝ
• dist_self : ∀ (x : α), dist x x = 0
• dist_comm : ∀ (x y : α), dist x y = dist y x
• dist_triangle : ∀ (x y z : α), dist x z ≤ dist x y + dist y z
• edist : α → α → ENNReal
• edist_dist : ∀ (x y : α), PseudoMetricSpace.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' : ∀ (a b : α), ‖a * b‖ = ‖a‖ * ‖b‖

  The norm is multiplicative.

@[instance 100]

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

A normed division ring is a normed ring.

Equations

• NormedDivisionRing.toNormedRing = NormedRing.mk ⋯ ⋯

@[instance 100]

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

A normed ring is a seminormed ring.

Equations

• NormedRing.toSeminormedRing = SeminormedRing.mk ⋯ ⋯

@[instance 100]

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

A normed ring is a non-unital normed ring.

Equations

• NormedRing.toNonUnitalNormedRing = NonUnitalNormedRing.mk ⋯ ⋯

class NonUnitalSeminormedCommRing (α : Type u_4) extends NonUnitalSeminormedRing α : Type u_4

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 : α), PseudoMetricSpace.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 : ∀ (a b : α), ‖a * b‖ ≤ ‖a‖ * ‖b‖
• mul_comm : ∀ (x y : α), x * y = y * x

  Multiplication is commutative.

class NonUnitalNormedCommRing (α : Type u_4) extends NonUnitalNormedRing α : Type u_4

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 : α), PseudoMetricSpace.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 : ∀ (a b : α), ‖a * b‖ ≤ ‖a‖ * ‖b‖
• mul_comm : ∀ (x y : α), x * y = y * x

  Multiplication is commutative.

@[instance 100]

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

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

Equations

• NonUnitalNormedCommRing.toNonUnitalSeminormedCommRing = NonUnitalSeminormedCommRing.mk ⋯

class SeminormedCommRing (α : Type u_4) extends SeminormedRing α : Type u_4

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 : α), PseudoMetricSpace.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 : ∀ (a b : α), ‖a * b‖ ≤ ‖a‖ * ‖b‖
• mul_comm : ∀ (x y : α), x * y = y * x

  Multiplication is commutative.

class NormedCommRing (α : Type u_4) extends NormedRing α : Type u_4

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 : α), PseudoMetricSpace.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 : ∀ (a b : α), ‖a * b‖ ≤ ‖a‖ * ‖b‖
• mul_comm : ∀ (x y : α), x * y = y * x

  Multiplication is commutative.

@[instance 100]

instance SeminormedCommRing.toNonUnitalSeminormedCommRing {α : Type u_1} [β : 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_1} [β : 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_1} [β : NormedCommRing α] : SeminormedCommRing α

A normed commutative ring is a seminormed commutative ring.

Equations

• NormedCommRing.toSeminormedCommRing = SeminormedCommRing.mk ⋯

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

Equations

• PUnit.normedCommRing = NormedCommRing.mk ⋯

class NormOneClass (α : Type u_4) [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.

@[simp]

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

theorem NormOneClass.nontrivial (α : Type u_4) [SeminormedAddCommGroup α] [One α] [NormOneClass α] : Nontrivial α

@[instance 100]

instance NonUnitalSeminormedCommRing.toNonUnitalCommRing {α : Type u_1} [β : NonUnitalSeminormedCommRing α] : NonUnitalCommRing α

Equations

• NonUnitalSeminormedCommRing.toNonUnitalCommRing = NonUnitalCommRing.mk ⋯

@[instance 100]

instance SeminormedCommRing.toCommRing {α : Type u_1} [β : SeminormedCommRing α] : CommRing α

Equations

• SeminormedCommRing.toCommRing = CommRing.mk ⋯

@[instance 100]

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

Equations

• NonUnitalNormedRing.toNormedAddCommGroup = NormedAddCommGroup.mk ⋯

@[instance 100]

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

Equations

• NonUnitalSeminormedRing.toSeminormedAddCommGroup = SeminormedAddCommGroup.mk ⋯

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

Equations

• ⋯ = ⋯

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

Equations

• ⋯ = ⋯

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

Equations

• ⋯ = ⋯

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

Equations

• ⋯ = ⋯

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

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

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

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

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

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

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

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

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

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

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

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

instance NonUnitalSubalgebra.nonUnitalSeminormedRing {𝕜 : Type u_4} [CommRing 𝕜] {E : Type u_5} [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_4} {𝕜 : Type u_5} {E : Type u_6} [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_4} [CommRing 𝕜] {E : Type u_5} [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_4} {𝕜 : Type u_5} {E : Type u_6} [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_1} [NonUnitalSeminormedRing α] : NonUnitalSeminormedRing (ULift.{u_4, u_1} α)

Equations

• ULift.nonUnitalSeminormedRing = NonUnitalSeminormedRing.mk ⋯ ⋯

instance Prod.nonUnitalSeminormedRing {α : Type u_1} {β : Type u_2} [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_1} [NonUnitalSeminormedRing α] : NonUnitalSeminormedRing αᵐᵒᵖ

Equations

• MulOpposite.instNonUnitalSeminormedRing = NonUnitalSeminormedRing.mk ⋯ ⋯

instance Subalgebra.seminormedRing {𝕜 : Type u_4} [CommRing 𝕜] {E : Type u_5} [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_4} {𝕜 : Type u_5} {E : Type u_6} [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_4} [CommRing 𝕜] {E : Type u_5} [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_4} {𝕜 : Type u_5} {E : Type u_6} [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_1} [SeminormedRing α] (n : ℕ) : ‖↑n‖ ≤ ↑n * ‖1‖

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

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

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

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

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

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

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

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

theorem nnnorm_pow_le' {α : Type u_1} [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_1} [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_1} [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_1} [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_1} [SeminormedRing α] (a : α) : ∀ᶠ (n : ℕ) in Filter.atTop, ‖a ^ n‖ ≤ ‖a‖ ^ n

instance ULift.seminormedRing {α : Type u_1} [SeminormedRing α] : SeminormedRing (ULift.{u_4, u_1} α)

Equations

• ULift.seminormedRing = SeminormedRing.mk ⋯ ⋯

instance Prod.seminormedRing {α : Type u_1} {β : Type u_2} [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_1} [SeminormedRing α] : SeminormedRing αᵐᵒᵖ

Equations

• MulOpposite.instSeminormedRing = SeminormedRing.mk ⋯ ⋯

theorem norm_sub_mul_le {α : Type u_1} [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_1} [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_1} [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_1} [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_1} [SeminormedRing α] (a b : αˣ) : ‖↑(a * b * a⁻¹ * b⁻¹) - 1‖ ≤ 2 * ‖↑a⁻¹‖ * ‖↑b⁻¹‖ * ‖↑a - 1‖ * ‖↑b - 1‖

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

def RingHom.IsBounded {α : Type u_4} [SeminormedRing α] {β : Type u_5} [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_1} [NonUnitalNormedRing α] : NonUnitalNormedRing (ULift.{u_4, u_1} α)

Equations

• ULift.nonUnitalNormedRing = NonUnitalNormedRing.mk ⋯ ⋯

instance Prod.nonUnitalNormedRing {α : Type u_1} {β : Type u_2} [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_1} [NonUnitalNormedRing α] : NonUnitalNormedRing αᵐᵒᵖ

Equations

• MulOpposite.instNonUnitalNormedRing = NonUnitalNormedRing.mk ⋯ ⋯

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

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

instance ULift.normedRing {α : Type u_1} [NormedRing α] : NormedRing (ULift.{u_4, u_1} α)

Equations

• ULift.normedRing = NormedRing.mk ⋯ ⋯

instance Prod.normedRing {α : Type u_1} {β : Type u_2} [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_1} [NormedRing α] : NormedRing αᵐᵒᵖ

Equations

• MulOpposite.instNormedRing = NormedRing.mk ⋯ ⋯

instance ULift.nonUnitalSeminormedCommRing {α : Type u_1} [NonUnitalSeminormedCommRing α] : NonUnitalSeminormedCommRing (ULift.{u_4, u_1} α)

Equations

• ULift.nonUnitalSeminormedCommRing = NonUnitalSeminormedCommRing.mk ⋯

instance Prod.nonUnitalSeminormedCommRing {α : Type u_1} {β : Type u_2} [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_1} [NonUnitalSeminormedCommRing α] : NonUnitalSeminormedCommRing αᵐᵒᵖ

Equations

• MulOpposite.instNonUnitalSeminormedCommRing = NonUnitalSeminormedCommRing.mk ⋯

instance NonUnitalSubalgebra.nonUnitalSeminormedCommRing {𝕜 : Type u_4} [CommRing 𝕜] {E : Type u_5} [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_4} [CommRing 𝕜] {E : Type u_5} [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_1} [NonUnitalNormedCommRing α] : NonUnitalNormedCommRing (ULift.{u_4, u_1} α)

Equations

• ULift.nonUnitalNormedCommRing = NonUnitalNormedCommRing.mk ⋯

instance Prod.nonUnitalNormedCommRing {α : Type u_1} {β : Type u_2} [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_1} [NonUnitalNormedCommRing α] : NonUnitalNormedCommRing αᵐᵒᵖ

Equations

• MulOpposite.instNonUnitalNormedCommRing = NonUnitalNormedCommRing.mk ⋯

instance ULift.seminormedCommRing {α : Type u_1} [SeminormedCommRing α] : SeminormedCommRing (ULift.{u_4, u_1} α)

Equations

• ULift.seminormedCommRing = SeminormedCommRing.mk ⋯

instance Prod.seminormedCommRing {α : Type u_1} {β : Type u_2} [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_1} [SeminormedCommRing α] : SeminormedCommRing αᵐᵒᵖ

Equations

• MulOpposite.instSeminormedCommRing = SeminormedCommRing.mk ⋯

instance Subalgebra.seminormedCommRing {𝕜 : Type u_4} [CommRing 𝕜] {E : Type u_5} [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_4} [CommRing 𝕜] {E : Type u_5} [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_1} [NormedCommRing α] : NormedCommRing (ULift.{u_4, u_1} α)

Equations

• ULift.normedCommRing = NormedCommRing.mk ⋯

instance Prod.normedCommRing {α : Type u_1} {β : Type u_2} [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_1} [NormedCommRing α] : NormedCommRing αᵐᵒᵖ

Equations

• MulOpposite.instNormedCommRing = NormedCommRing.mk ⋯

theorem IsPowMul.restriction {R : Type u_4} {S : Type u_5} [NormedCommRing R] [CommRing 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.

@[simp]

theorem norm_mul {α : Type u_1} [NormedDivisionRing α] (a b : α) : ‖a * b‖ = ‖a‖ * ‖b‖

@[instance 900]

instance NormedDivisionRing.to_normOneClass {α : Type u_1} [NormedDivisionRing α] : NormOneClass α

Equations

• ⋯ = ⋯

instance isAbsoluteValue_norm {α : Type u_1} [NormedDivisionRing α] : IsAbsoluteValue norm

Equations

• ⋯ = ⋯

@[simp]

theorem nnnorm_mul {α : Type u_1} [NormedDivisionRing α] (a b : α) : ‖a * b‖₊ = ‖a‖₊ * ‖b‖₊

def normHom {α : Type u_1} [NormedDivisionRing α] : α →*₀ ℝ

norm as a MonoidWithZeroHom.

Equations

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

@[simp]

theorem normHom_apply {α : Type u_1} [NormedDivisionRing α] (x✝ : α) : normHom x✝ = ‖x✝‖

def nnnormHom {α : Type u_1} [NormedDivisionRing α] : α →*₀ NNReal

nnnorm as a MonoidWithZeroHom.

Equations

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

@[simp]

theorem nnnormHom_apply {α : Type u_1} [NormedDivisionRing α] (x✝ : α) : nnnormHom x✝ = ‖x✝‖₊

@[simp]

theorem norm_pow {α : Type u_1} [NormedDivisionRing α] (a : α) (n : ℕ) : ‖a ^ n‖ = ‖a‖ ^ n

@[simp]

theorem nnnorm_pow {α : Type u_1} [NormedDivisionRing α] (a : α) (n : ℕ) : ‖a ^ n‖₊ = ‖a‖₊ ^ n

theorem List.norm_prod {α : Type u_1} [NormedDivisionRing α] (l : List α) : ‖l.prod‖ = (List.map norm l).prod

theorem List.nnnorm_prod {α : Type u_1} [NormedDivisionRing α] (l : List α) : ‖l.prod‖₊ = (List.map nnnorm l).prod

@[simp]

theorem norm_div {α : Type u_1} [NormedDivisionRing α] (a b : α) : ‖a / b‖ = ‖a‖ / ‖b‖

@[simp]

theorem nnnorm_div {α : Type u_1} [NormedDivisionRing α] (a b : α) : ‖a / b‖₊ = ‖a‖₊ / ‖b‖₊

@[simp]

theorem norm_inv {α : Type u_1} [NormedDivisionRing α] (a : α) : ‖a⁻¹‖ = ‖a‖⁻¹

@[simp]

theorem nnnorm_inv {α : Type u_1} [NormedDivisionRing α] (a : α) : ‖a⁻¹‖₊ = ‖a‖₊⁻¹

@[simp]

theorem norm_zpow {α : Type u_1} [NormedDivisionRing α] (a : α) (n : ℤ) : ‖a ^ n‖ = ‖a‖ ^ n

@[simp]

theorem nnnorm_zpow {α : Type u_1} [NormedDivisionRing α] (a : α) (n : ℤ) : ‖a ^ n‖₊ = ‖a‖₊ ^ n

theorem dist_inv_inv₀ {α : Type u_1} [NormedDivisionRing α] {z w : α} (hz : z ≠ 0) (hw : w ≠ 0) : dist z⁻¹ w⁻¹ = dist z w / (‖z‖ * ‖w‖)

theorem nndist_inv_inv₀ {α : Type u_1} [NormedDivisionRing α] {z w : α} (hz : z ≠ 0) (hw : w ≠ 0) : nndist z⁻¹ w⁻¹ = nndist z w / (‖z‖₊ * ‖w‖₊)

theorem norm_commutator_sub_one_le {α : Type u_1} [NormedDivisionRing α] {a b : α} (ha : a ≠ 0) (hb : b ≠ 0) : ‖a * b * a⁻¹ * b⁻¹ - 1‖ ≤ 2 * ‖a‖⁻¹ * ‖b‖⁻¹ * ‖a - 1‖ * ‖b - 1‖

theorem nnnorm_commutator_sub_one_le {α : Type u_1} [NormedDivisionRing α] {a b : α} (ha : a ≠ 0) (hb : b ≠ 0) : ‖a * b * a⁻¹ * b⁻¹ - 1‖₊ ≤ 2 * ‖a‖₊⁻¹ * ‖b‖₊⁻¹ * ‖a - 1‖₊ * ‖b - 1‖₊

theorem NormedDivisionRing.norm_eq_one_iff_ne_zero_of_discrete {𝕜 : Type u_4} [NormedDivisionRing 𝕜] [DiscreteTopology 𝕜] {x : 𝕜} : ‖x‖ = 1 ↔ x ≠ 0

@[simp]

theorem NormedDivisionRing.norm_le_one_of_discrete {𝕜 : Type u_4} [NormedDivisionRing 𝕜] [DiscreteTopology 𝕜] (x : 𝕜) : ‖x‖ ≤ 1

theorem NormedDivisionRing.discreteTopology_unit_closedBall_eq_univ {𝕜 : Type u_4} [NormedDivisionRing 𝕜] [DiscreteTopology 𝕜] : Metric.closedBall 0 1 = Set.univ

class NormedField (α : Type u_4) extends Norm α, Field α, MetricSpace α : Type u_4

A normed field is a field with a norm satisfying ‖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)
• mul_comm : ∀ (a b : α), a * b = b * a
• inv : α → α
• div : α → α → α
• div_eq_mul_inv : ∀ (a b : α), a / b = a * b⁻¹
• zpow : ℤ → α → α
• zpow_zero' : ∀ (a : α), Field.zpow 0 a = 1
• zpow_succ' : ∀ (n : ℕ) (a : α), Field.zpow (↑n.succ) a = Field.zpow (↑n) a * a
• zpow_neg' : ∀ (n : ℕ) (a : α), Field.zpow (Int.negSucc n) a = (Field.zpow (↑n.succ) a)⁻¹
• exists_pair_ne : ∃ (x : α) (y : α), x ≠ y
• nnratCast : ℚ≥0 → α
• ratCast : ℚ → α
• mul_inv_cancel : ∀ (a : α), a ≠ 0 → a * a⁻¹ = 1
• inv_zero : 0⁻¹ = 0
• nnratCast_def : ∀ (q : ℚ≥0), ↑q = ↑q.num / ↑q.den
• nnqsmul : ℚ≥0 → α → α
• nnqsmul_def : ∀ (q : ℚ≥0) (a : α), Field.nnqsmul q a = ↑q * a
• ratCast_def : ∀ (q : ℚ), ↑q = ↑q.num / ↑q.den
• qsmul : ℚ → α → α
• qsmul_def : ∀ (a : ℚ) (x : α), Field.qsmul a x = ↑a * x
• dist : α → α → ℝ
• dist_self : ∀ (x : α), dist x x = 0
• dist_comm : ∀ (x y : α), dist x y = dist y x
• dist_triangle : ∀ (x y z : α), dist x z ≤ dist x y + dist y z
• edist : α → α → ENNReal
• edist_dist : ∀ (x y : α), PseudoMetricSpace.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' : ∀ (a b : α), ‖a * b‖ = ‖a‖ * ‖b‖

  The norm is multiplicative.

class NontriviallyNormedField (α : Type u_4) extends NormedField α : Type u_4

A nontrivially normed field is a normed field in which there is an element of norm different from 0 and 1. This makes it possible to bring any element arbitrarily close to 0 by multiplication by the powers of any element, and thus to relate algebra and topology.

• norm : α → ℝ
• add : α → α → α
• 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)
• mul_comm : ∀ (a b : α), a * b = b * a
• inv : α → α
• div : α → α → α
• div_eq_mul_inv : ∀ (a b : α), a / b = a * b⁻¹
• zpow : ℤ → α → α
• zpow_zero' : ∀ (a : α), Field.zpow 0 a = 1
• zpow_succ' : ∀ (n : ℕ) (a : α), Field.zpow (↑n.succ) a = Field.zpow (↑n) a * a
• zpow_neg' : ∀ (n : ℕ) (a : α), Field.zpow (Int.negSucc n) a = (Field.zpow (↑n.succ) a)⁻¹
• exists_pair_ne : ∃ (x : α) (y : α), x ≠ y
• nnratCast : ℚ≥0 → α
• ratCast : ℚ → α
• mul_inv_cancel : ∀ (a : α), a ≠ 0 → a * a⁻¹ = 1
• inv_zero : 0⁻¹ = 0
• nnratCast_def : ∀ (q : ℚ≥0), ↑q = ↑q.num / ↑q.den
• nnqsmul : ℚ≥0 → α → α
• nnqsmul_def : ∀ (q : ℚ≥0) (a : α), Field.nnqsmul q a = ↑q * a
• ratCast_def : ∀ (q : ℚ), ↑q = ↑q.num / ↑q.den
• qsmul : ℚ → α → α
• qsmul_def : ∀ (a : ℚ) (x : α), Field.qsmul a x = ↑a * x
• dist : α → α → ℝ
• dist_self : ∀ (x : α), dist x x = 0
• dist_comm : ∀ (x y : α), dist x y = dist y x
• dist_triangle : ∀ (x y z : α), dist x z ≤ dist x y + dist y z
• edist : α → α → ENNReal
• edist_dist : ∀ (x y : α), PseudoMetricSpace.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' : ∀ (a b : α), ‖a * b‖ = ‖a‖ * ‖b‖
• non_trivial : ∃ (x : α), 1 < ‖x‖

  The norm attains a value exceeding 1.

class DenselyNormedField (α : Type u_4) extends NormedField α : Type u_4

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

• norm : α → ℝ
• add : α → α → α
• 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)
• mul_comm : ∀ (a b : α), a * b = b * a
• inv : α → α
• div : α → α → α
• div_eq_mul_inv : ∀ (a b : α), a / b = a * b⁻¹
• zpow : ℤ → α → α
• zpow_zero' : ∀ (a : α), Field.zpow 0 a = 1
• zpow_succ' : ∀ (n : ℕ) (a : α), Field.zpow (↑n.succ) a = Field.zpow (↑n) a * a
• zpow_neg' : ∀ (n : ℕ) (a : α), Field.zpow (Int.negSucc n) a = (Field.zpow (↑n.succ) a)⁻¹
• exists_pair_ne : ∃ (x : α) (y : α), x ≠ y
• nnratCast : ℚ≥0 → α
• ratCast : ℚ → α
• mul_inv_cancel : ∀ (a : α), a ≠ 0 → a * a⁻¹ = 1
• inv_zero : 0⁻¹ = 0
• nnratCast_def : ∀ (q : ℚ≥0), ↑q = ↑q.num / ↑q.den
• nnqsmul : ℚ≥0 → α → α
• nnqsmul_def : ∀ (q : ℚ≥0) (a : α), Field.nnqsmul q a = ↑q * a
• ratCast_def : ∀ (q : ℚ), ↑q = ↑q.num / ↑q.den
• qsmul : ℚ → α → α
• qsmul_def : ∀ (a : ℚ) (x : α), Field.qsmul a x = ↑a * x
• dist : α → α → ℝ
• dist_self : ∀ (x : α), dist x x = 0
• dist_comm : ∀ (x y : α), dist x y = dist y x
• dist_triangle : ∀ (x y z : α), dist x z ≤ dist x y + dist y z
• edist : α → α → ENNReal
• edist_dist : ∀ (x y : α), PseudoMetricSpace.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' : ∀ (a b : α), ‖a * b‖ = ‖a‖ * ‖b‖
• lt_norm_lt : ∀ (x y : ℝ), 0 ≤ x → x < y → ∃ (a : α), x < ‖a‖ ∧ ‖a‖ < y

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

@[instance 100]

instance DenselyNormedField.toNontriviallyNormedField {α : Type u_1} [DenselyNormedField α] : NontriviallyNormedField α

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

Equations

• DenselyNormedField.toNontriviallyNormedField = NontriviallyNormedField.mk ⋯

@[instance 100]

instance NormedField.toNormedDivisionRing {α : Type u_1} [NormedField α] : NormedDivisionRing α

Equations

• NormedField.toNormedDivisionRing = NormedDivisionRing.mk ⋯ ⋯

@[instance 100]

instance NormedField.toNormedCommRing {α : Type u_1} [NormedField α] : NormedCommRing α

Equations

• NormedField.toNormedCommRing = NormedCommRing.mk ⋯

@[simp]

theorem norm_prod {α : Type u_1} {β : Type u_2} [NormedField α] (s : Finset β) (f : β → α) : ‖∏ b ∈ s, f b‖ = ∏ b ∈ s, ‖f b‖

@[simp]

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

theorem NormedField.exists_one_lt_norm (α : Type u_1) [NontriviallyNormedField α] : ∃ (x : α), 1 < ‖x‖

theorem NormedField.exists_lt_norm (α : Type u_1) [NontriviallyNormedField α] (r : ℝ) : ∃ (x : α), r < ‖x‖

theorem NormedField.exists_norm_lt (α : Type u_1) [NontriviallyNormedField α] {r : ℝ} (hr : 0 < r) : ∃ (x : α), 0 < ‖x‖ ∧ ‖x‖ < r

theorem NormedField.exists_norm_lt_one (α : Type u_1) [NontriviallyNormedField α] : ∃ (x : α), 0 < ‖x‖ ∧ ‖x‖ < 1

theorem NormedField.punctured_nhds_neBot {α : Type u_1} [NontriviallyNormedField α] (x : α) : (nhdsWithin x {x}ᶜ).NeBot

theorem NormedField.nhdsWithin_isUnit_neBot {α : Type u_1} [NontriviallyNormedField α] : (nhdsWithin 0 {x : α | IsUnit x}).NeBot

theorem NormedField.exists_lt_norm_lt (α : Type u_1) [DenselyNormedField α] {r₁ r₂ : ℝ} (h₀ : 0 ≤ r₁) (h : r₁ < r₂) : ∃ (x : α), r₁ < ‖x‖ ∧ ‖x‖ < r₂

theorem NormedField.exists_lt_nnnorm_lt (α : Type u_1) [DenselyNormedField α] {r₁ r₂ : NNReal} (h : r₁ < r₂) : ∃ (x : α), r₁ < ‖x‖₊ ∧ ‖x‖₊ < r₂

instance NormedField.denselyOrdered_range_norm (α : Type u_1) [DenselyNormedField α] : DenselyOrdered ↑(Set.range norm)

Equations

• ⋯ = ⋯

instance NormedField.denselyOrdered_range_nnnorm (α : Type u_1) [DenselyNormedField α] : DenselyOrdered ↑(Set.range nnnorm)

Equations

• ⋯ = ⋯

def NontriviallyNormedField.ofNormNeOne {𝕜 : Type u_4} [h' : NormedField 𝕜] (h : ∃ (x : 𝕜), x ≠ 0 ∧ ‖x‖ ≠ 1) : NontriviallyNormedField 𝕜

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

Equations

• NontriviallyNormedField.ofNormNeOne h = NontriviallyNormedField.mk ⋯

instance Real.normedCommRing : NormedCommRing ℝ

Equations

• Real.normedCommRing = NormedCommRing.mk ⋯

noncomputable instance Real.normedField : NormedField ℝ

Equations

• Real.normedField = NormedField.mk ⋯ ⋯

noncomputable instance Real.denselyNormedField : DenselyNormedField ℝ

Equations

• Real.denselyNormedField = DenselyNormedField.mk Real.denselyNormedField.proof_1

theorem Real.toNNReal_mul_nnnorm {x : ℝ} (y : ℝ) (hx : 0 ≤ x) : x.toNNReal * ‖y‖₊ = ‖x * y‖₊

theorem Real.nnnorm_mul_toNNReal (x : ℝ) {y : ℝ} (hy : 0 ≤ y) : ‖x‖₊ * y.toNNReal = ‖x * y‖₊

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

@[simp]

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

@[simp]

theorem norm_norm {α : Type u_1} [SeminormedAddCommGroup α] (x : α) : ‖‖x‖‖ = ‖x‖

@[simp]

theorem nnnorm_norm {α : Type u_1} [SeminormedAddCommGroup α] (a : α) : ‖‖a‖‖₊ = ‖a‖₊

theorem NormedAddCommGroup.tendsto_atTop {α : Type u_1} [Nonempty α] [Preorder α] [IsDirected α fun (x1 x2 : α) => x1 ≤ x2] {β : Type u_4} [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_1} [Nonempty α] [Preorder α] [IsDirected α fun (x1 x2 : α) => x1 ≤ x2] [NoMaxOrder α] {β : Type u_4} [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_4} {R₂ : Type u_5} [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.

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

Equations

• ⋯ = ⋯

Induced normed structures

@[reducible, inline]

abbrev NonUnitalSeminormedRing.induced {F : Type u_4} (R : Type u_5) (S : Type u_6) [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_4} (R : Type u_5) (S : Type u_6) [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_4} (R : Type u_5) (S : Type u_6) [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_4} (R : Type u_5) (S : Type u_6) [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_4} (R : Type u_5) (S : Type u_6) [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_4} (R : Type u_5) (S : Type u_6) [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_4} (R : Type u_5) (S : Type u_6) [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_4} (R : Type u_5) (S : Type u_6) [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 ⋯

@[reducible, inline]

abbrev NormedDivisionRing.induced {F : Type u_4} (R : Type u_5) (S : Type u_6) [FunLike F R S] [DivisionRing R] [NormedDivisionRing S] [NonUnitalRingHomClass F R S] (f : F) (hf : Function.Injective ⇑f) : NormedDivisionRing R

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

See note [reducible non-instances]

Equations

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

@[reducible, inline]

abbrev NormedField.induced {F : Type u_4} (R : Type u_5) (S : Type u_6) [FunLike F R S] [Field R] [NormedField S] [NonUnitalRingHomClass F R S] (f : F) (hf : Function.Injective ⇑f) : NormedField R

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

See note [reducible non-instances]

Equations

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

theorem NormOneClass.induced {F : Type u_7} (R : Type u_8) (S : Type u_9) [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.

instance SubringClass.toSeminormedRing {S : Type u_4} {R : Type u_5} [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_4} {R : Type u_5} [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_4} {R : Type u_5} [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_4} {R : Type u_5} [SetLike S R] [NormedCommRing R] [SubringClass S R] (s : S) : NormedCommRing ↥s

Equations

• SubringClass.toNormedCommRing s = NormedCommRing.mk ⋯

instance SubfieldClass.toNormedField {S : Type u_4} {F : Type u_5} [SetLike S F] [NormedField F] [SubfieldClass S F] (s : S) : NormedField ↥s

If s is a subfield of a normed field F, then s is equipped with an induced normed field structure.

Equations

• SubfieldClass.toNormedField s = NormedField.induced (↥s) F (SubringClass.subtype s) ⋯

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

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

Equations

• v.toNormedRing = NormedRing.mk ⋯ ⋯

noncomputable def AbsoluteValue.toNormedField {K : Type u_4} [Field K] (v : AbsoluteValue K ℝ) : NormedField K

A real absolute value on a field determines a NormedField structure.

Equations

• v.toNormedField = NormedField.mk ⋯ ⋯