Normed fields

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

class NonUnitalSeminormedRing (α : Type u_5) extends 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 (Int.ofNat n.succ) a = SubNegMonoid.zsmul (Int.ofNat n) a + a
• zsmul_neg' : ∀ (n : ℕ) (a : α), SubNegMonoid.zsmul (Int.negSucc n) a = -SubNegMonoid.zsmul (↑n.succ) a
• add_left_neg : ∀ (a : α), -a + a = 0
• add_comm : ∀ (a b : α), a + b = b + a
• mul : α → α → α
• left_distrib : ∀ (a b c : α), a * (b + c) = a * b + a * c
• right_distrib : ∀ (a b c : α), (a + b) * c = a * c + b * c
• zero_mul : ∀ (a : α), 0 * a = 0
• mul_zero : ∀ (a : α), a * 0 = 0
• mul_assoc : ∀ (a b c : α), a * b * c = a * (b * c)
• dist : α → α → ℝ
• dist_self : ∀ (x : α), dist x x = 0
• dist_comm : ∀ (x y : α), dist x y = dist y x
• dist_triangle : ∀ (x y z : α), dist x z ≤ dist x y + dist y z
• edist : α → α → ENNReal
• edist_dist : ∀ (x y : α), 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.

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

The distance is induced by the norm.

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

The norm is submultiplicative.

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

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

• norm : α → ℝ
• add : α → α → α
• add_assoc : ∀ (a b c : α), a + b + c = a + (b + c)
• zero : α
• zero_add : ∀ (a : α), 0 + a = a
• add_zero : ∀ (a : α), a + 0 = a
• nsmul : ℕ → α → α
• nsmul_zero : ∀ (x : α), AddMonoid.nsmul 0 x = 0
• nsmul_succ : ∀ (n : ℕ) (x : α), AddMonoid.nsmul (n + 1) x = AddMonoid.nsmul n x + x
• add_comm : ∀ (a b : α), a + b = b + a
• mul : α → α → α
• left_distrib : ∀ (a b c : α), a * (b + c) = a * b + a * c
• right_distrib : ∀ (a b c : α), (a + b) * c = a * c + b * c
• zero_mul : ∀ (a : α), 0 * a = 0
• mul_zero : ∀ (a : α), a * 0 = 0
• mul_assoc : ∀ (a b c : α), a * b * c = a * (b * c)
• one : α
• one_mul : ∀ (a : α), 1 * a = a
• mul_one : ∀ (a : α), a * 1 = a
• natCast : ℕ → α
• natCast_zero : NatCast.natCast 0 = 0
• natCast_succ : ∀ (n : ℕ), NatCast.natCast (n + 1) = NatCast.natCast n + 1
• npow : ℕ → α → α
• npow_zero : ∀ (x : α), Semiring.npow 0 x = 1
• npow_succ : ∀ (n : ℕ) (x : α), Semiring.npow (n + 1) x = Semiring.npow n x * x
• neg : α → α
• sub : α → α → α
• sub_eq_add_neg : ∀ (a b : α), a - b = a + -b
• zsmul : ℤ → α → α
• zsmul_zero' : ∀ (a : α), Ring.zsmul 0 a = 0
• zsmul_succ' : ∀ (n : ℕ) (a : α), Ring.zsmul (Int.ofNat n.succ) a = Ring.zsmul (Int.ofNat n) a + a
• zsmul_neg' : ∀ (n : ℕ) (a : α), Ring.zsmul (Int.negSucc n) a = -Ring.zsmul (↑n.succ) a
• add_left_neg : ∀ (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.

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

The distance is induced by the norm.

theorem SeminormedRing.norm_mul {α : Type u_5} [self : SeminormedRing α] (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_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 (Int.ofNat n.succ) a = SubNegMonoid.zsmul (Int.ofNat n) a + a
• zsmul_neg' : ∀ (n : ℕ) (a : α), SubNegMonoid.zsmul (Int.negSucc n) a = -SubNegMonoid.zsmul (↑n.succ) a
• add_left_neg : ∀ (a : α), -a + a = 0
• add_comm : ∀ (a b : α), a + b = b + a
• mul : α → α → α
• left_distrib : ∀ (a b c : α), a * (b + c) = a * b + a * c
• right_distrib : ∀ (a b c : α), (a + b) * c = a * c + b * c
• zero_mul : ∀ (a : α), 0 * a = 0
• mul_zero : ∀ (a : α), a * 0 = 0
• mul_assoc : ∀ (a b c : α), a * b * c = a * (b * c)
• dist : α → α → ℝ
• dist_self : ∀ (x : α), dist x x = 0
• dist_comm : ∀ (x y : α), dist x y = dist y x
• dist_triangle : ∀ (x y z : α), dist x z ≤ dist x y + dist y z
• edist : α → α → ENNReal
• edist_dist : ∀ (x y : α), 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.

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

The distance is induced by the norm.

theorem NonUnitalNormedRing.norm_mul {α : Type u_5} [self : NonUnitalNormedRing α] (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_5) extends Norm , Ring , MetricSpace : Type u_5

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

• norm : α → ℝ
• add : α → α → α
• add_assoc : ∀ (a b c : α), a + b + c = a + (b + c)
• zero : α
• zero_add : ∀ (a : α), 0 + a = a
• add_zero : ∀ (a : α), a + 0 = a
• nsmul : ℕ → α → α
• nsmul_zero : ∀ (x : α), AddMonoid.nsmul 0 x = 0
• nsmul_succ : ∀ (n : ℕ) (x : α), AddMonoid.nsmul (n + 1) x = AddMonoid.nsmul n x + x
• add_comm : ∀ (a b : α), a + b = b + a
• mul : α → α → α
• left_distrib : ∀ (a b c : α), a * (b + c) = a * b + a * c
• right_distrib : ∀ (a b c : α), (a + b) * c = a * c + b * c
• zero_mul : ∀ (a : α), 0 * a = 0
• mul_zero : ∀ (a : α), a * 0 = 0
• mul_assoc : ∀ (a b c : α), a * b * c = a * (b * c)
• one : α
• one_mul : ∀ (a : α), 1 * a = a
• mul_one : ∀ (a : α), a * 1 = a
• natCast : ℕ → α
• natCast_zero : NatCast.natCast 0 = 0
• natCast_succ : ∀ (n : ℕ), NatCast.natCast (n + 1) = NatCast.natCast n + 1
• npow : ℕ → α → α
• npow_zero : ∀ (x : α), Semiring.npow 0 x = 1
• npow_succ : ∀ (n : ℕ) (x : α), Semiring.npow (n + 1) x = Semiring.npow n x * x
• neg : α → α
• sub : α → α → α
• sub_eq_add_neg : ∀ (a b : α), a - b = a + -b
• zsmul : ℤ → α → α
• zsmul_zero' : ∀ (a : α), Ring.zsmul 0 a = 0
• zsmul_succ' : ∀ (n : ℕ) (a : α), Ring.zsmul (Int.ofNat n.succ) a = Ring.zsmul (Int.ofNat n) a + a
• zsmul_neg' : ∀ (n : ℕ) (a : α), Ring.zsmul (Int.negSucc n) a = -Ring.zsmul (↑n.succ) a
• add_left_neg : ∀ (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.

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

The distance is induced by the norm.

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

The norm is submultiplicative.

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

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

• norm : α → ℝ
• add : α → α → α
• 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 (Int.ofNat n.succ) a = Ring.zsmul (Int.ofNat n) a + a
• zsmul_neg' : ∀ (n : ℕ) (a : α), Ring.zsmul (Int.negSucc n) a = -Ring.zsmul (↑n.succ) a
• add_left_neg : ∀ (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 (Int.ofNat n.succ) a = DivisionRing.zpow (Int.ofNat 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.

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

The distance is induced by the norm.

theorem NormedDivisionRing.norm_mul' {α : Type u_5} [self : NormedDivisionRing α] (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_5) extends NonUnitalSeminormedRing : 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 (Int.ofNat n.succ) a = SubNegMonoid.zsmul (Int.ofNat n) a + a
• zsmul_neg' : ∀ (n : ℕ) (a : α), SubNegMonoid.zsmul (Int.negSucc n) a = -SubNegMonoid.zsmul (↑n.succ) a
• add_left_neg : ∀ (a : α), -a + a = 0
• add_comm : ∀ (a b : α), a + b = b + a
• mul : α → α → α
• left_distrib : ∀ (a b c : α), a * (b + c) = a * b + a * c
• right_distrib : ∀ (a b c : α), (a + b) * c = a * c + b * c
• zero_mul : ∀ (a : α), 0 * a = 0
• mul_zero : ∀ (a : α), a * 0 = 0
• mul_assoc : ∀ (a b c : α), a * b * c = a * (b * c)
• dist : α → α → ℝ
• dist_self : ∀ (x : α), dist x x = 0
• dist_comm : ∀ (x y : α), dist x y = dist y x
• dist_triangle : ∀ (x y z : α), dist x z ≤ dist x y + dist y z
• edist : α → α → ENNReal
• edist_dist : ∀ (x y : α), 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.

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

Multiplication is commutative.

class NonUnitalNormedCommRing (α : Type u_5) extends NonUnitalNormedRing : 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 (Int.ofNat n.succ) a = SubNegMonoid.zsmul (Int.ofNat n) a + a
• zsmul_neg' : ∀ (n : ℕ) (a : α), SubNegMonoid.zsmul (Int.negSucc n) a = -SubNegMonoid.zsmul (↑n.succ) a
• add_left_neg : ∀ (a : α), -a + a = 0
• add_comm : ∀ (a b : α), a + b = b + a
• mul : α → α → α
• left_distrib : ∀ (a b c : α), a * (b + c) = a * b + a * c
• right_distrib : ∀ (a b c : α), (a + b) * c = a * c + b * c
• zero_mul : ∀ (a : α), 0 * a = 0
• mul_zero : ∀ (a : α), a * 0 = 0
• mul_assoc : ∀ (a b c : α), a * b * c = a * (b * c)
• dist : α → α → ℝ
• dist_self : ∀ (x : α), dist x x = 0
• dist_comm : ∀ (x y : α), dist x y = dist y x
• dist_triangle : ∀ (x y z : α), dist x z ≤ dist x y + dist y z
• edist : α → α → ENNReal
• edist_dist : ∀ (x y : α), 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.

theorem NonUnitalNormedCommRing.mul_comm {α : Type u_5} [self : NonUnitalNormedCommRing α] (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_5) extends SeminormedRing : Type u_5

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

• norm : α → ℝ
• add : α → α → α
• add_assoc : ∀ (a b c : α), a + b + c = a + (b + c)
• zero : α
• zero_add : ∀ (a : α), 0 + a = a
• add_zero : ∀ (a : α), a + 0 = a
• nsmul : ℕ → α → α
• nsmul_zero : ∀ (x : α), AddMonoid.nsmul 0 x = 0
• nsmul_succ : ∀ (n : ℕ) (x : α), AddMonoid.nsmul (n + 1) x = AddMonoid.nsmul n x + x
• add_comm : ∀ (a b : α), a + b = b + a
• mul : α → α → α
• left_distrib : ∀ (a b c : α), a * (b + c) = a * b + a * c
• right_distrib : ∀ (a b c : α), (a + b) * c = a * c + b * c
• zero_mul : ∀ (a : α), 0 * a = 0
• mul_zero : ∀ (a : α), a * 0 = 0
• mul_assoc : ∀ (a b c : α), a * b * c = a * (b * c)
• one : α
• one_mul : ∀ (a : α), 1 * a = a
• mul_one : ∀ (a : α), a * 1 = a
• natCast : ℕ → α
• natCast_zero : NatCast.natCast 0 = 0
• natCast_succ : ∀ (n : ℕ), NatCast.natCast (n + 1) = NatCast.natCast n + 1
• npow : ℕ → α → α
• npow_zero : ∀ (x : α), Semiring.npow 0 x = 1
• npow_succ : ∀ (n : ℕ) (x : α), Semiring.npow (n + 1) x = Semiring.npow n x * x
• neg : α → α
• sub : α → α → α
• sub_eq_add_neg : ∀ (a b : α), a - b = a + -b
• zsmul : ℤ → α → α
• zsmul_zero' : ∀ (a : α), Ring.zsmul 0 a = 0
• zsmul_succ' : ∀ (n : ℕ) (a : α), Ring.zsmul (Int.ofNat n.succ) a = Ring.zsmul (Int.ofNat n) a + a
• zsmul_neg' : ∀ (n : ℕ) (a : α), Ring.zsmul (Int.negSucc n) a = -Ring.zsmul (↑n.succ) a
• add_left_neg : ∀ (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.

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

Multiplication is commutative.

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

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

• norm : α → ℝ
• add : α → α → α
• add_assoc : ∀ (a b c : α), a + b + c = a + (b + c)
• zero : α
• zero_add : ∀ (a : α), 0 + a = a
• add_zero : ∀ (a : α), a + 0 = a
• nsmul : ℕ → α → α
• nsmul_zero : ∀ (x : α), AddMonoid.nsmul 0 x = 0
• nsmul_succ : ∀ (n : ℕ) (x : α), AddMonoid.nsmul (n + 1) x = AddMonoid.nsmul n x + x
• add_comm : ∀ (a b : α), a + b = b + a
• mul : α → α → α
• left_distrib : ∀ (a b c : α), a * (b + c) = a * b + a * c
• right_distrib : ∀ (a b c : α), (a + b) * c = a * c + b * c
• zero_mul : ∀ (a : α), 0 * a = 0
• mul_zero : ∀ (a : α), a * 0 = 0
• mul_assoc : ∀ (a b c : α), a * b * c = a * (b * c)
• one : α
• one_mul : ∀ (a : α), 1 * a = a
• mul_one : ∀ (a : α), a * 1 = a
• natCast : ℕ → α
• natCast_zero : NatCast.natCast 0 = 0
• natCast_succ : ∀ (n : ℕ), NatCast.natCast (n + 1) = NatCast.natCast n + 1
• npow : ℕ → α → α
• npow_zero : ∀ (x : α), Semiring.npow 0 x = 1
• npow_succ : ∀ (n : ℕ) (x : α), Semiring.npow (n + 1) x = Semiring.npow n x * x
• neg : α → α
• sub : α → α → α
• sub_eq_add_neg : ∀ (a b : α), a - b = a + -b
• zsmul : ℤ → α → α
• zsmul_zero' : ∀ (a : α), Ring.zsmul 0 a = 0
• zsmul_succ' : ∀ (n : ℕ) (a : α), Ring.zsmul (Int.ofNat n.succ) a = Ring.zsmul (Int.ofNat n) a + a
• zsmul_neg' : ∀ (n : ℕ) (a : α), Ring.zsmul (Int.negSucc n) a = -Ring.zsmul (↑n.succ) a
• add_left_neg : ∀ (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.

theorem NormedCommRing.mul_comm {α : Type u_5} [self : NormedCommRing α] (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_5 + 1}

Equations

• PUnit.normedCommRing = let __src := PUnit.normedAddCommGroup; let __src_1 := PUnit.commRing; NormedCommRing.mk ⋯

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

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

• norm_one : ‖1‖ = 1

  The norm of the multiplicative identity is 1.

@[simp]

theorem NormOneClass.norm_one {α : Type u_5} [Norm α] [One α] [self : NormOneClass α] : ‖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_5) [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 = let __src := inst; SeminormedAddCommGroup.mk ⋯

instance ULift.normOneClass {α : Type u_1} [SeminormedAddCommGroup α] [One α] [NormOneClass α] : NormOneClass (ULift.{u_5, 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_5} {α : ι → Type u_6} [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 one_le_norm_one (β : Type u_5) [NormedRing β] [Nontrivial β] : 1 ≤ ‖1‖

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

theorem Filter.Tendsto.zero_mul_isBoundedUnder_le {α : Type u_1} {ι : Type u_4} [NonUnitalSeminormedRing α] {f : ι → α} {g : ι → α} {l : Filter ι} (hf : Filter.Tendsto f l (nhds 0)) (hg : Filter.IsBoundedUnder (fun (x x_1 : ℝ) => x ≤ x_1) l ((fun (x : α) => ‖x‖) ∘ g)) : Filter.Tendsto (fun (x : ι) => f x * g x) l (nhds 0)

theorem Filter.isBoundedUnder_le_mul_tendsto_zero {α : Type u_1} {ι : Type u_4} [NonUnitalSeminormedRing α] {f : ι → α} {g : ι → α} {l : Filter ι} (hf : Filter.IsBoundedUnder (fun (x x_1 : ℝ) => x ≤ x_1) l (norm ∘ f)) (hg : Filter.Tendsto g l (nhds 0)) : Filter.Tendsto (fun (x : ι) => f x * g x) l (nhds 0)

theorem mulLeft_bound {α : Type u_1} [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_5} [CommRing 𝕜] {E : Type u_6} [NonUnitalSeminormedRing E] [Module 𝕜 E] (s : NonUnitalSubalgebra 𝕜 E) : NonUnitalSeminormedRing ↥s

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

Equations

• s.nonUnitalSeminormedRing = let __src := s.toSubmodule.seminormedAddCommGroup; let __src_1 := s.toNonUnitalRing; NonUnitalSeminormedRing.mk ⋯ ⋯

instance NonUnitalSubalgebra.nonUnitalNormedRing {𝕜 : Type u_5} [CommRing 𝕜] {E : Type u_6} [NonUnitalNormedRing E] [Module 𝕜 E] (s : NonUnitalSubalgebra 𝕜 E) : NonUnitalNormedRing ↥s

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

Equations

• s.nonUnitalNormedRing = let __src := s.nonUnitalSeminormedRing; NonUnitalNormedRing.mk ⋯ ⋯

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

Equations

• ULift.nonUnitalSeminormedRing = let __src := ULift.seminormedAddCommGroup; let __src_1 := ULift.nonUnitalRing; 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 = let __src := Prod.seminormedAddCommGroup; let __src_1 := Prod.instNonUnitalRing; NonUnitalSeminormedRing.mk ⋯ ⋯

instance Pi.nonUnitalSeminormedRing {ι : Type u_4} {π : ι → Type u_5} [Fintype ι] [(i : ι) → NonUnitalSeminormedRing (π i)] : NonUnitalSeminormedRing ((i : ι) → π i)

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

Equations

• Pi.nonUnitalSeminormedRing = let __src := Pi.seminormedAddCommGroup; let __src_1 := Pi.nonUnitalRing; NonUnitalSeminormedRing.mk ⋯ ⋯

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

Equations

• MulOpposite.instNonUnitalSeminormedRing = let __spread.0 := MulOpposite.instNonUnitalRing; let __spread.1 := MulOpposite.instSeminormedAddCommGroup; NonUnitalSeminormedRing.mk ⋯ ⋯

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

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

Equations

• s.seminormedRing = let __src := (Subalgebra.toSubmodule s).seminormedAddCommGroup; let __src_1 := s.toRing; SeminormedRing.mk ⋯ ⋯

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

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

Equations

• s.normedRing = let __src := s.seminormedRing; 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_4} {α : Type u_5} [NormedCommRing α] (s : Finset ι) (hs : s.Nonempty) (f : ι → α) : ‖∏ i ∈ s, f i‖ ≤ ∏ i ∈ s, ‖f i‖

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

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

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

theorem nnnorm_pow_le' {α : Type u_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_5, u_1} α)

Equations

• ULift.seminormedRing = let __src := ULift.nonUnitalSeminormedRing; let __src_1 := ULift.ring; 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 = let __src := Prod.nonUnitalSeminormedRing; let __src_1 := Prod.instRing; SeminormedRing.mk ⋯ ⋯

instance Pi.seminormedRing {ι : Type u_4} {π : ι → Type u_5} [Fintype ι] [(i : ι) → SeminormedRing (π i)] : SeminormedRing ((i : ι) → π i)

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

Equations

• Pi.seminormedRing = let __src := Pi.nonUnitalSeminormedRing; let __src_1 := Pi.ring; SeminormedRing.mk ⋯ ⋯

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

Equations

• MulOpposite.instSeminormedRing = let __spread.0 := MulOpposite.instRing; let __spread.1 := MulOpposite.instNonUnitalSeminormedRing; SeminormedRing.mk ⋯ ⋯

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

Equations

• ULift.nonUnitalNormedRing = let __src := ULift.nonUnitalSeminormedRing; let __src_1 := ULift.normedAddCommGroup; 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 = let __src := Prod.nonUnitalSeminormedRing; let __src_1 := Prod.normedAddCommGroup; NonUnitalNormedRing.mk ⋯ ⋯

instance Pi.nonUnitalNormedRing {ι : Type u_4} {π : ι → Type u_5} [Fintype ι] [(i : ι) → NonUnitalNormedRing (π i)] : NonUnitalNormedRing ((i : ι) → π i)

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

Equations

• Pi.nonUnitalNormedRing = let __src := Pi.nonUnitalSeminormedRing; let __src_1 := Pi.normedAddCommGroup; NonUnitalNormedRing.mk ⋯ ⋯

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

Equations

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

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_5, u_1} α)

Equations

• ULift.normedRing = let __src := ULift.seminormedRing; let __src_1 := ULift.normedAddCommGroup; 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 = let __src := Prod.nonUnitalNormedRing; let __src_1 := Prod.instRing; NormedRing.mk ⋯ ⋯

instance Pi.normedRing {ι : Type u_4} {π : ι → Type u_5} [Fintype ι] [(i : ι) → NormedRing (π i)] : NormedRing ((i : ι) → π i)

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

Equations

• Pi.normedRing = let __src := Pi.seminormedRing; let __src_1 := Pi.normedAddCommGroup; NormedRing.mk ⋯ ⋯

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

Equations

• MulOpposite.instNormedRing = let __spread.0 := MulOpposite.instRing; let __spread.1 := MulOpposite.instSeminormedRing; let __spread.2 := MulOpposite.instNormedAddCommGroup; NormedRing.mk ⋯ ⋯

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

Equations

• ULift.nonUnitalSeminormedCommRing = let __src := ULift.nonUnitalSeminormedRing; let __src_1 := ULift.nonUnitalCommRing; 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 = let __src := Prod.nonUnitalSeminormedRing; let __src_1 := Prod.instNonUnitalCommRing; NonUnitalSeminormedCommRing.mk ⋯

instance Pi.nonUnitalSeminormedCommRing {ι : Type u_4} {π : ι → Type u_5} [Fintype ι] [(i : ι) → NonUnitalSeminormedCommRing (π i)] : NonUnitalSeminormedCommRing ((i : ι) → π i)

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

Equations

• Pi.nonUnitalSeminormedCommRing = let __src := Pi.nonUnitalSeminormedRing; let __src_1 := Pi.nonUnitalCommRing; NonUnitalSeminormedCommRing.mk ⋯

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

Equations

• MulOpposite.instNonUnitalSeminormedCommRing = let __spread.0 := MulOpposite.instNonUnitalSeminormedRing; let __spread.1 := MulOpposite.instNonUnitalCommRing; NonUnitalSeminormedCommRing.mk ⋯

instance NonUnitalSubalgebra.nonUnitalSeminormedCommRing {𝕜 : Type u_5} [CommRing 𝕜] {E : Type u_6} [NonUnitalSeminormedCommRing E] [Module 𝕜 E] (s : NonUnitalSubalgebra 𝕜 E) : NonUnitalSeminormedCommRing ↥s

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

Equations

• s.nonUnitalSeminormedCommRing = let __src := s.nonUnitalSeminormedRing; let __src_1 := s.toNonUnitalCommRing; NonUnitalSeminormedCommRing.mk ⋯

instance NonUnitalSubalgebra.nonUnitalNormedCommRing {𝕜 : Type u_5} [CommRing 𝕜] {E : Type u_6} [NonUnitalNormedCommRing E] [Module 𝕜 E] (s : NonUnitalSubalgebra 𝕜 E) : NonUnitalNormedCommRing ↥s

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

Equations

• s.nonUnitalNormedCommRing = let __src := s.nonUnitalSeminormedCommRing; let __src_1 := s.nonUnitalNormedRing; NonUnitalNormedCommRing.mk ⋯

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

Equations

• ULift.nonUnitalNormedCommRing = let __src := ULift.nonUnitalSeminormedCommRing; let __src_1 := ULift.normedAddCommGroup; 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 = let __src := Prod.nonUnitalSeminormedCommRing; let __src_1 := Prod.normedAddCommGroup; NonUnitalNormedCommRing.mk ⋯

instance Pi.nonUnitalNormedCommRing {ι : Type u_4} {π : ι → Type u_5} [Fintype ι] [(i : ι) → NonUnitalNormedCommRing (π i)] : NonUnitalNormedCommRing ((i : ι) → π i)

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

Equations

• Pi.nonUnitalNormedCommRing = let __src := Pi.nonUnitalSeminormedCommRing; let __src_1 := Pi.normedAddCommGroup; NonUnitalNormedCommRing.mk ⋯

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

Equations

• MulOpposite.instNonUnitalNormedCommRing = let __spread.0 := MulOpposite.instNonUnitalNormedRing; let __spread.1 := MulOpposite.instNonUnitalSeminormedCommRing; NonUnitalNormedCommRing.mk ⋯

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

Equations

• ULift.seminormedCommRing = let __src := ULift.nonUnitalSeminormedRing; let __src_1 := ULift.commRing; 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 = let __src := Prod.nonUnitalSeminormedCommRing; let __src_1 := Prod.instCommRing; SeminormedCommRing.mk ⋯

instance Pi.seminormedCommRing {ι : Type u_4} {π : ι → Type u_5} [Fintype ι] [(i : ι) → SeminormedCommRing (π i)] : SeminormedCommRing ((i : ι) → π i)

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

Equations

• Pi.seminormedCommRing = let __src := Pi.nonUnitalSeminormedCommRing; let __src_1 := Pi.ring; SeminormedCommRing.mk ⋯

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

Equations

• MulOpposite.instSeminormedCommRing = let __spread.0 := MulOpposite.instSeminormedRing; let __spread.1 := MulOpposite.instNonUnitalSeminormedCommRing; SeminormedCommRing.mk ⋯

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

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

Equations

• s.seminormedCommRing = let __src := s.seminormedRing; let __src_1 := s.toCommRing; SeminormedCommRing.mk ⋯

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

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

Equations

• s.normedCommRing = let __src := s.seminormedCommRing; let __src_1 := s.normedRing; NormedCommRing.mk ⋯

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

Equations

• ULift.normedCommRing = let __src := ULift.normedRing; let __src_1 := ULift.seminormedCommRing; 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 = let __src := Prod.nonUnitalNormedRing; let __src_1 := Prod.instCommRing; NormedCommRing.mk ⋯

instance Pi.normedCommutativeRing {ι : Type u_4} {π : ι → Type u_5} [Fintype ι] [(i : ι) → NormedCommRing (π i)] : NormedCommRing ((i : ι) → π i)

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

Equations

• Pi.normedCommutativeRing = let __src := Pi.seminormedCommRing; let __src_1 := Pi.normedAddCommGroup; NormedCommRing.mk ⋯

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

Equations

• MulOpposite.instNormedCommRing = let __spread.0 := MulOpposite.instNormedRing; let __spread.1 := MulOpposite.instSeminormedCommRing; NormedCommRing.mk ⋯

@[instance 100]

instance semi_normed_ring_top_monoid {α : Type u_1} [NonUnitalSeminormedRing α] : ContinuousMul α

Equations

• ⋯ = ⋯

@[instance 100]

instance semi_normed_top_ring {α : Type u_1} [NonUnitalSeminormedRing α] : TopologicalRing α

A seminormed ring is a topological ring.

Equations

• ⋯ = ⋯

@[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‖₊

@[simp]

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

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

norm as a MonoidWithZeroHom.

Equations

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

@[simp]

theorem nnnormHom_apply {α : Type u_1} [NormedDivisionRing α] : ∀ (x : α), nnnormHom 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 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 antilipschitzWith_mul_left {α : Type u_1} [NormedDivisionRing α] {a : α} (ha : a ≠ 0) : AntilipschitzWith ‖a‖₊⁻¹ fun (x : α) => a * x

theorem antilipschitzWith_mul_right {α : Type u_1} [NormedDivisionRing α] {a : α} (ha : a ≠ 0) : AntilipschitzWith ‖a‖₊⁻¹ fun (x : α) => x * a

@[simp]

theorem DilationEquiv.mulLeft_symm_apply {α : Type u_1} [NormedDivisionRing α] (a : α) (ha : a ≠ 0) (x : α) : (DilationEquiv.mulLeft a ha).symm x = a⁻¹ * x

@[simp]

theorem DilationEquiv.mulLeft_apply {α : Type u_1} [NormedDivisionRing α] (a : α) (ha : a ≠ 0) (x : α) : (DilationEquiv.mulLeft a ha) x = a * x

def DilationEquiv.mulLeft {α : Type u_1} [NormedDivisionRing α] (a : α) (ha : a ≠ 0) : α ≃ᵈ α

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

Equations

• DilationEquiv.mulLeft a ha = { toEquiv := Equiv.mulLeft₀ a ha, edist_eq' := ⋯ }

@[simp]

theorem DilationEquiv.mulRight_symm_apply {α : Type u_1} [NormedDivisionRing α] (a : α) (ha : a ≠ 0) (x : α) : (DilationEquiv.mulRight a ha).symm x = x * a⁻¹

@[simp]

theorem DilationEquiv.mulRight_apply {α : Type u_1} [NormedDivisionRing α] (a : α) (ha : a ≠ 0) (x : α) : (DilationEquiv.mulRight a ha) x = x * a

def DilationEquiv.mulRight {α : Type u_1} [NormedDivisionRing α] (a : α) (ha : a ≠ 0) : α ≃ᵈ α

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

Equations

• DilationEquiv.mulRight a ha = { toEquiv := Equiv.mulRight₀ a ha, edist_eq' := ⋯ }

@[simp]

theorem Filter.comap_mul_left_cobounded {α : Type u_1} [NormedDivisionRing α] {a : α} (ha : a ≠ 0) : Filter.comap (fun (x : α) => a * x) (Bornology.cobounded α) = Bornology.cobounded α

@[simp]

theorem Filter.map_mul_left_cobounded {α : Type u_1} [NormedDivisionRing α] {a : α} (ha : a ≠ 0) : Filter.map (fun (x : α) => a * x) (Bornology.cobounded α) = Bornology.cobounded α

@[simp]

theorem Filter.comap_mul_right_cobounded {α : Type u_1} [NormedDivisionRing α] {a : α} (ha : a ≠ 0) : Filter.comap (fun (x : α) => x * a) (Bornology.cobounded α) = Bornology.cobounded α

@[simp]

theorem Filter.map_mul_right_cobounded {α : Type u_1} [NormedDivisionRing α] {a : α} (ha : a ≠ 0) : Filter.map (fun (x : α) => x * a) (Bornology.cobounded α) = Bornology.cobounded α

theorem Filter.tendsto_mul_left_cobounded {α : Type u_1} [NormedDivisionRing α] {a : α} (ha : a ≠ 0) : Filter.Tendsto (fun (x : α) => a * x) (Bornology.cobounded α) (Bornology.cobounded α)

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

theorem Filter.tendsto_mul_right_cobounded {α : Type u_1} [NormedDivisionRing α] {a : α} (ha : a ≠ 0) : Filter.Tendsto (fun (x : α) => x * a) (Bornology.cobounded α) (Bornology.cobounded α)

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

@[simp]

theorem Filter.inv_cobounded₀ {α : Type u_1} [NormedDivisionRing α] : (Bornology.cobounded α)⁻¹ = nhdsWithin 0 {0}ᶜ

@[simp]

theorem Filter.inv_nhdsWithin_ne_zero {α : Type u_1} [NormedDivisionRing α] : (nhdsWithin 0 {0}ᶜ)⁻¹ = Bornology.cobounded α

theorem Filter.tendsto_inv₀_cobounded' {α : Type u_1} [NormedDivisionRing α] : Filter.Tendsto Inv.inv (Bornology.cobounded α) (nhdsWithin 0 {0}ᶜ)

theorem Filter.tendsto_inv₀_cobounded {α : Type u_1} [NormedDivisionRing α] : Filter.Tendsto Inv.inv (Bornology.cobounded α) (nhds 0)

theorem Filter.tendsto_inv₀_nhdsWithin_ne_zero {α : Type u_1} [NormedDivisionRing α] : Filter.Tendsto Inv.inv (nhdsWithin 0 {0}ᶜ) (Bornology.cobounded α)

@[instance 100]

instance NormedDivisionRing.to_hasContinuousInv₀ {α : Type u_1} [NormedDivisionRing α] : HasContinuousInv₀ α

Equations

• ⋯ = ⋯

@[instance 100]

instance NormedDivisionRing.to_topologicalDivisionRing {α : Type u_1} [NormedDivisionRing α] : TopologicalDivisionRing α

A normed division ring is a topological division ring.

Equations

• ⋯ = ⋯

theorem IsOfFinOrder.norm_eq_one {α : Type u_1} [NormedDivisionRing α] {a : α} (ha : IsOfFinOrder a) : ‖a‖ = 1

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

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 (Int.ofNat n.succ) a = Ring.zsmul (Int.ofNat n) a + a
• zsmul_neg' : ∀ (n : ℕ) (a : α), Ring.zsmul (Int.negSucc n) a = -Ring.zsmul (↑n.succ) a
• add_left_neg : ∀ (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 (Int.ofNat n.succ) a = Field.zpow (Int.ofNat 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.

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

The distance is induced by the norm.

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

The norm is multiplicative.

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

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

• norm : α → ℝ
• add : α → α → α
• 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 (Int.ofNat n.succ) a = Ring.zsmul (Int.ofNat n) a + a
• zsmul_neg' : ∀ (n : ℕ) (a : α), Ring.zsmul (Int.negSucc n) a = -Ring.zsmul (↑n.succ) a
• add_left_neg : ∀ (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 (Int.ofNat n.succ) a = Field.zpow (Int.ofNat 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.

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

The norm attains a value exceeding 1.

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

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

• norm : α → ℝ
• add : α → α → α
• 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 (Int.ofNat n.succ) a = Ring.zsmul (Int.ofNat n) a + a
• zsmul_neg' : ∀ (n : ℕ) (a : α), Ring.zsmul (Int.negSucc n) a = -Ring.zsmul (↑n.succ) a
• add_left_neg : ∀ (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 (Int.ofNat n.succ) a = Field.zpow (Int.ofNat 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.

theorem DenselyNormedField.lt_norm_lt {α : Type u_5} [self : DenselyNormedField α] (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 = let __src := inst; NormedDivisionRing.mk ⋯ ⋯

@[instance 100]

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

Equations

• NormedField.toNormedCommRing = let __src := inst; 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₁ : NNReal} {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

• ⋯ = ⋯

theorem NormedField.denseRange_nnnorm (α : Type u_1) [DenselyNormedField α] : DenseRange nnnorm

def NontriviallyNormedField.ofNormNeOne {𝕜 : Type u_5} [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 = let __src := Real.normedAddCommGroup; let __src_1 := Real.commRing; NormedCommRing.mk ⋯

noncomputable instance Real.normedField : NormedField ℝ

Equations

• Real.normedField = let __src := Real.normedAddCommGroup; let __src_1 := Real.field; 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

theorem NNReal.lipschitzWith_sub : LipschitzWith 2 fun (p : NNReal × NNReal) => p.1 - p.2

@[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 α] [SemilatticeSup α] {β : Type u_5} [SeminormedAddCommGroup β] {f : α → β} {b : β} : Filter.Tendsto f Filter.atTop (nhds b) ↔ ∀ (ε : ℝ), 0 < ε → ∃ (N : α), ∀ (n : α), N ≤ n → ‖f n - b‖ < ε

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

theorem NormedAddCommGroup.tendsto_atTop' {α : Type u_1} [Nonempty α] [SemilatticeSup α] [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, ...

instance Int.instNormedCommRing : NormedCommRing ℤ

Equations

• Int.instNormedCommRing = let __spread.0 := Int.instCommRing; let __spread.1 := Int.instNormedAddCommGroup; NormedCommRing.mk ⋯

instance Int.instNormOneClass : NormOneClass ℤ

Equations

• Int.instNormOneClass = ⋯

instance Rat.instNormedField : NormedField ℚ

Equations

• Rat.instNormedField = let __spread.0 := Rat.instField; let __spread.1 := Rat.instNormedAddCommGroup; NormedField.mk ⋯ Rat.instNormedField.proof_1

instance Rat.instDenselyNormedField : DenselyNormedField ℚ

Equations

• Rat.instDenselyNormedField = DenselyNormedField.mk Rat.instDenselyNormedField.proof_1

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

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

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

  The ring homomorphism is an isometry.

@[simp]

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

The ring homomorphism is an isometry.

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

Equations

• ⋯ = ⋯

Induced normed structures

@[reducible, inline]

abbrev NonUnitalSeminormedRing.induced {F : Type u_5} (R : Type u_6) (S : Type u_7) [FunLike F R S] [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 = let __src := SeminormedAddCommGroup.induced R S f; let __src_1 := inst✝¹; NonUnitalSeminormedRing.mk ⋯ ⋯

@[reducible, inline]

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

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

See note [reducible non-instances]

Equations

• NonUnitalNormedRing.induced R S f hf = let __src := NonUnitalSeminormedRing.induced R S f; let __src_1 := NormedAddCommGroup.induced R S f hf; NonUnitalNormedRing.mk ⋯ ⋯

@[reducible, inline]

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

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

See note [reducible non-instances]

Equations

• SeminormedRing.induced R S f = let __src := NonUnitalSeminormedRing.induced R S f; let __src_1 := SeminormedAddCommGroup.induced R S f; let __src_2 := inst✝¹; SeminormedRing.mk ⋯ ⋯

@[reducible, inline]

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

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

See note [reducible non-instances]

Equations

• NormedRing.induced R S f hf = let __src := NonUnitalSeminormedRing.induced R S f; let __src_1 := NormedAddCommGroup.induced R S f hf; let __src_2 := inst✝¹; NormedRing.mk ⋯ ⋯

@[reducible, inline]

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

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

See note [reducible non-instances]

Equations

• NonUnitalSeminormedCommRing.induced R S f = let __src := NonUnitalSeminormedRing.induced R S f; let __src_1 := inst✝¹; NonUnitalSeminormedCommRing.mk ⋯

@[reducible, inline]

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

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

See note [reducible non-instances]

Equations

• NonUnitalNormedCommRing.induced R S f hf = let __src := NonUnitalNormedRing.induced R S f hf; let __src_1 := inst✝¹; NonUnitalNormedCommRing.mk ⋯

@[reducible, inline]

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

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

See note [reducible non-instances]

Equations

• SeminormedCommRing.induced R S f = let __src := NonUnitalSeminormedRing.induced R S f; let __src_1 := SeminormedAddCommGroup.induced R S f; let __src_2 := inst✝¹; SeminormedCommRing.mk ⋯

@[reducible, inline]

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

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

See note [reducible non-instances]

Equations

• NormedCommRing.induced R S f hf = let __src := SeminormedCommRing.induced R S f; let __src_1 := NormedAddCommGroup.induced R S f hf; NormedCommRing.mk ⋯

@[reducible, inline]

abbrev NormedDivisionRing.induced {F : Type u_5} (R : Type u_6) (S : Type u_7) [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 = let __src := NormedAddCommGroup.induced R S f hf; let __src_1 := inst✝¹; NormedDivisionRing.mk ⋯ ⋯

@[reducible, inline]

abbrev NormedField.induced {F : Type u_5} (R : Type u_6) (S : Type u_7) [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 = let __src := NormedDivisionRing.induced R S f hf; NormedField.mk ⋯ ⋯

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

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

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

Equations

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

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

Equations

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

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

Equations

• SubringClass.toSeminormedCommRing s = let __src := SubringClass.toSeminormedRing s; SeminormedCommRing.mk ⋯

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

Equations

• SubringClass.toNormedCommRing s = let __src := SubringClass.toNormedRing s; NormedCommRing.mk ⋯