Normed division rings and fields

In this file we define normed fields, and (more generally) normed division rings. 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 field instance from a given real absolute value on a field are given in:

• AbsoluteValue.toNormedField

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 : ↑0 = 0
• natCast_succ (n : ℕ) : ↑(n + 1) = ↑n + 1
• npow : ℕ → α → α
• npow_zero (x : α) : Semiring.npow 0 x = 1
• npow_succ (n : ℕ) (x : α) : Semiring.npow (n + 1) x = Semiring.npow n x * x
• neg : α → α
• sub : α → α → α
• sub_eq_add_neg (a b : α) : a - b = a + -b
• zsmul : ℤ → α → α
• zsmul_zero' (a : α) : Ring.zsmul 0 a = 0
• zsmul_succ' (n : ℕ) (a : α) : Ring.zsmul (↑n.succ) a = Ring.zsmul (↑n) a + a
• zsmul_neg' (n : ℕ) (a : α) : Ring.zsmul (Int.negSucc n) a = -Ring.zsmul (↑n.succ) a
• neg_add_cancel (a : α) : -a + a = 0
• intCast : ℤ → α
• intCast_ofNat (n : ℕ) : IntCast.intCast ↑n = ↑n
• intCast_negSucc (n : ℕ) : IntCast.intCast (Int.negSucc n) = -↑(n + 1)
• 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 : α) : 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_2} [β : NormedDivisionRing α] : NormedRing α

A normed division ring is a normed ring.

Equations

• NormedDivisionRing.toNormedRing = { toNorm := NormedDivisionRing.toNorm, toRing := DivisionRing.toRing, toMetricSpace := NormedDivisionRing.toMetricSpace, dist_eq := ⋯, norm_mul_le := ⋯ }

@[instance 100]

instance NormedDivisionRing.toNormMulClass {α : Type u_2} [NormedDivisionRing α] : NormMulClass α

The norm on a normed division ring is strictly multiplicative.

@[instance 900]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

theorem enorm_inv {α : Type u_2} [NormedDivisionRing α] {a : α} (ha : a ≠ 0) : ‖a⁻¹‖ₑ = ‖a‖ₑ⁻¹

@[simp]

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

@[simp]

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

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

theorem nndist_inv_inv₀ {α : Type u_2} [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_2} [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_2} [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_5} [NormedDivisionRing 𝕜] [DiscreteTopology 𝕜] {x : 𝕜} : ‖x‖ = 1 ↔ x ≠ 0

@[simp]

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

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

@[deprecated NormedDivisionRing.unitClosedBall_eq_univ_of_discrete (since := "2024-12-01")]

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

Alias of NormedDivisionRing.unitClosedBall_eq_univ_of_discrete.

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 : ↑0 = 0
• natCast_succ (n : ℕ) : ↑(n + 1) = ↑n + 1
• npow : ℕ → α → α
• npow_zero (x : α) : Semiring.npow 0 x = 1
• npow_succ (n : ℕ) (x : α) : Semiring.npow (n + 1) x = Semiring.npow n x * x
• neg : α → α
• sub : α → α → α
• sub_eq_add_neg (a b : α) : a - b = a + -b
• zsmul : ℤ → α → α
• zsmul_zero' (a : α) : Ring.zsmul 0 a = 0
• zsmul_succ' (n : ℕ) (a : α) : Ring.zsmul (↑n.succ) a = Ring.zsmul (↑n) a + a
• zsmul_neg' (n : ℕ) (a : α) : Ring.zsmul (Int.negSucc n) a = -Ring.zsmul (↑n.succ) a
• neg_add_cancel (a : α) : -a + a = 0
• intCast : ℤ → α
• intCast_ofNat (n : ℕ) : IntCast.intCast ↑n = ↑n
• intCast_negSucc (n : ℕ) : IntCast.intCast (Int.negSucc n) = -↑(n + 1)
• 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 : α) : 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_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 : ↑0 = 0
• natCast_succ (n : ℕ) : ↑(n + 1) = ↑n + 1
• npow : ℕ → α → α
• npow_zero (x : α) : Semiring.npow 0 x = 1
• npow_succ (n : ℕ) (x : α) : Semiring.npow (n + 1) x = Semiring.npow n x * x
• neg : α → α
• sub : α → α → α
• sub_eq_add_neg (a b : α) : a - b = a + -b
• zsmul : ℤ → α → α
• zsmul_zero' (a : α) : Ring.zsmul 0 a = 0
• zsmul_succ' (n : ℕ) (a : α) : Ring.zsmul (↑n.succ) a = Ring.zsmul (↑n) a + a
• zsmul_neg' (n : ℕ) (a : α) : Ring.zsmul (Int.negSucc n) a = -Ring.zsmul (↑n.succ) a
• neg_add_cancel (a : α) : -a + a = 0
• intCast : ℤ → α
• intCast_ofNat (n : ℕ) : IntCast.intCast ↑n = ↑n
• intCast_negSucc (n : ℕ) : IntCast.intCast (Int.negSucc n) = -↑(n + 1)
• 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 : α) : 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_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 : ↑0 = 0
• natCast_succ (n : ℕ) : ↑(n + 1) = ↑n + 1
• npow : ℕ → α → α
• npow_zero (x : α) : Semiring.npow 0 x = 1
• npow_succ (n : ℕ) (x : α) : Semiring.npow (n + 1) x = Semiring.npow n x * x
• neg : α → α
• sub : α → α → α
• sub_eq_add_neg (a b : α) : a - b = a + -b
• zsmul : ℤ → α → α
• zsmul_zero' (a : α) : Ring.zsmul 0 a = 0
• zsmul_succ' (n : ℕ) (a : α) : Ring.zsmul (↑n.succ) a = Ring.zsmul (↑n) a + a
• zsmul_neg' (n : ℕ) (a : α) : Ring.zsmul (Int.negSucc n) a = -Ring.zsmul (↑n.succ) a
• neg_add_cancel (a : α) : -a + a = 0
• intCast : ℤ → α
• intCast_ofNat (n : ℕ) : IntCast.intCast ↑n = ↑n
• intCast_negSucc (n : ℕ) : IntCast.intCast (Int.negSucc n) = -↑(n + 1)
• 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 : α) : 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_2} [DenselyNormedField α] : NontriviallyNormedField α

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

Equations

• DenselyNormedField.toNontriviallyNormedField = { toNormedField := DenselyNormedField.toNormedField, non_trivial := ⋯ }

@[instance 100]

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

Equations

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

@[instance 100]

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

Equations

• NormedField.toNormedCommRing = { toNorm := NormedField.toNorm, toRing := CommRing.toRing, toMetricSpace := NormedField.toMetricSpace, dist_eq := ⋯, norm_mul_le := ⋯, mul_comm := ⋯ }

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

theorem NormedField.exists_one_lt_nnnorm (α : Type u_2) [NontriviallyNormedField α] : ∃ (x : α), 1 < ‖x‖₊

theorem NormedField.exists_one_lt_enorm (α : Type u_2) [NontriviallyNormedField α] : ∃ (x : α), 1 < ‖x‖ₑ

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

theorem NormedField.exists_lt_nnnorm (α : Type u_2) [NontriviallyNormedField α] (r : NNReal) : ∃ (x : α), r < ‖x‖₊

theorem NormedField.exists_lt_enorm (α : Type u_2) [NontriviallyNormedField α] {r : ENNReal} (hr : r ≠ ⊤) : ∃ (x : α), r < ‖x‖ₑ

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

theorem NormedField.exists_nnnorm_lt (α : Type u_2) [NontriviallyNormedField α] {r : NNReal} (hr : 0 < r) : ∃ (x : α), 0 < ‖x‖₊ ∧ ‖x‖₊ < r

theorem NormedField.exists_enorm_lt (α : Type u_2) [NontriviallyNormedField α] {r : ENNReal} (hr : 0 < r) : ∃ (x : α), 0 < ‖x‖ₑ ∧ ‖x‖ₑ < r

TODO: merge with _root_.exists_enorm_lt.

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

theorem NormedField.exists_nnnorm_lt_one (α : Type u_2) [NontriviallyNormedField α] : ∃ (x : α), 0 < ‖x‖₊ ∧ ‖x‖₊ < 1

theorem NormedField.exists_enorm_lt_one (α : Type u_2) [NontriviallyNormedField α] : ∃ (x : α), 0 < ‖x‖ₑ ∧ ‖x‖ₑ < 1

instance NormedField.nhdsNE_neBot {α : Type u_2} [NontriviallyNormedField α] (x : α) : (nhdsWithin x {x}ᶜ).NeBot

@[deprecated NormedField.nhdsNE_neBot (since := "2025-03-02")]

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

Alias of NormedField.nhdsNE_neBot.

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

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

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

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

instance NormedField.denselyOrdered_range_nnnorm (α : Type u_2) [DenselyNormedField α] : DenselyOrdered ↑(Set.range 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 = { toNormedField := h', non_trivial := ⋯ }

noncomputable instance Real.normedField : NormedField ℝ

Equations

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

noncomputable instance Real.denselyNormedField : DenselyNormedField ℝ

Equations

• Real.denselyNormedField = { toNormedField := Real.normedField, lt_norm_lt := Real.denselyNormedField._proof_38 }

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

Induced normed structures

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

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

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

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

instance SubfieldClass.toNormedField {S : Type u_5} {F : Type u_6} [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.toNormedField {K : Type u_5} [Field K] (v : AbsoluteValue K ℝ) : NormedField K

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

Equations

• v.toNormedField = { toNorm := NormedRing.toNorm, toField := inferInstanceAs (Field K), toMetricSpace := NormedRing.toMetricSpace, dist_eq := ⋯, norm_mul := ⋯ }