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

@[instance 100]

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

A normed division ring is a normed ring.

Equations

• NormedDivisionRing.toNormedRing = { toNorm := β.toNorm, toRing := β.toRing, toMetricSpace := β.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

@[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 := inst✝.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 := inst✝.toNorm, toRing := inst✝.toRing, toMetricSpace := inst✝.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_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‖₊

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 := v.toNormedRing.toNorm, toField := inferInstanceAs (Field K), toMetricSpace := v.toNormedRing.toMetricSpace, dist_eq := ⋯, norm_mul := ⋯ }