Normed fields

In this file we continue building the theory of normed division rings and fields.

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

• discreteTopology_or_nontriviallyNormedField
• discreteTopology_of_bddAbove_range_norm

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.

@[simp]

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

@[simp]

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

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.

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

theorem Filter.tendsto_mul_left_cobounded {α : Type u_1} [NormedDivisionRing α] {a : α} (ha : a ≠ 0) : 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) : 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 α] : Tendsto Inv.inv (Bornology.cobounded α) (nhdsWithin 0 {0}ᶜ)

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

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

@[instance 100]

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

@[instance 100]

instance NormedDivisionRing.to_isTopologicalDivisionRing {α : Type u_1} [NormedDivisionRing α] : IsTopologicalDivisionRing α

A normed division ring is a topological division ring.

@[deprecated NormedDivisionRing.to_isTopologicalDivisionRing (since := "2025-03-25")]

theorem NormedDivisionRing.to_topologicalDivisionRing {α : Type u_1} [NormedDivisionRing α] : IsTopologicalDivisionRing α

Alias of NormedDivisionRing.to_isTopologicalDivisionRing.

---

A normed division ring is a topological division ring.

theorem NormedField.tendsto_norm_inv_nhdsNE_zero_atTop {α : Type u_1} [NormedDivisionRing α] : Filter.Tendsto (fun (x : α) => ‖x⁻¹‖) (nhdsWithin 0 {0}ᶜ) Filter.atTop

@[deprecated NormedField.tendsto_norm_inv_nhdsNE_zero_atTop (since := "2024-12-22")]

theorem NormedField.tendsto_norm_inverse_nhdsWithin_0_atTop {α : Type u_1} [NormedDivisionRing α] : Filter.Tendsto (fun (x : α) => ‖x⁻¹‖) (nhdsWithin 0 {0}ᶜ) Filter.atTop

Alias of NormedField.tendsto_norm_inv_nhdsNE_zero_atTop.

theorem NormedField.tendsto_norm_zpow_nhdsNE_zero_atTop {α : Type u_1} [NormedDivisionRing α] {m : ℤ} (hm : m < 0) : Filter.Tendsto (fun (x : α) => ‖x ^ m‖) (nhdsWithin 0 {0}ᶜ) Filter.atTop

@[deprecated NormedField.tendsto_norm_zpow_nhdsNE_zero_atTop (since := "2024-12-22")]

theorem NormedField.tendsto_norm_zpow_nhdsWithin_0_atTop {α : Type u_1} [NormedDivisionRing α] {m : ℤ} (hm : m < 0) : Filter.Tendsto (fun (x : α) => ‖x ^ m‖) (nhdsWithin 0 {0}ᶜ) Filter.atTop

Alias of NormedField.tendsto_norm_zpow_nhdsNE_zero_atTop.

theorem NormedField.discreteTopology_or_nontriviallyNormedField (𝕜 : Type u_4) [h : NormedField 𝕜] : DiscreteTopology 𝕜 ∨ Nonempty { h' : NontriviallyNormedField 𝕜 // h'.toNormedField = h }

A normed field is either nontrivially normed or has a discrete topology. In the discrete topology case, all the norms are 1, by norm_eq_one_iff_ne_zero_of_discrete. The nontrivially normed field instance is provided by a subtype with a proof that the forgetful inheritance to the existing NormedField instance is definitionally true. This allows one to have the new NontriviallyNormedField instance without data clashes.

theorem NormedField.discreteTopology_of_bddAbove_range_norm {𝕜 : Type u_4} [NormedField 𝕜] (h : BddAbove (Set.range fun (k : 𝕜) => ‖k‖)) : DiscreteTopology 𝕜

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

@[simp]

theorem NormedField.continuousAt_zpow {𝕜 : Type u_4} [NontriviallyNormedField 𝕜] {n : ℤ} {x : 𝕜} : ContinuousAt (fun (x : 𝕜) => x ^ n) x ↔ x ≠ 0 ∨ 0 ≤ n

@[simp]

theorem NormedField.continuousAt_inv {𝕜 : Type u_4} [NontriviallyNormedField 𝕜] {x : 𝕜} : ContinuousAt Inv.inv x ↔ x ≠ 0

instance Rat.instNormedField : NormedField ℚ

instance Rat.instDenselyNormedField : DenselyNormedField ℚ

theorem NormedField.completeSpace_iff_isComplete_closedBall {K : Type u_4} [NormedField K] : CompleteSpace K ↔ IsComplete (Metric.closedBall 0 1)