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_nhdsNE_zero {α : Type u_1} [NormedDivisionRing α] : (nhdsWithin 0 {0}ᶜ)⁻¹ = Bornology.cobounded α

@[deprecated Filter.inv_nhdsNE_zero (since := "2025-11-26")]

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

Alias of Filter.inv_nhdsNE_zero.

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₀_nhdsNE_zero {α : Type u_1} [NormedDivisionRing α] : Tendsto Inv.inv (nhdsWithin 0 {0}ᶜ) (Bornology.cobounded α)

@[deprecated Filter.tendsto_inv₀_nhdsNE_zero (since := "2025-11-26")]

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

Alias of Filter.tendsto_inv₀_nhdsNE_zero.

theorem uniformContinuousOn_inv₀ {α : Type u_1} [NormedDivisionRing α] {s : Set α} (hs : sᶜ ∈ nhds 0) : UniformContinuousOn Inv.inv s

If s is a set disjoint from 𝓝 0, then fun x ↦ x⁻¹ is uniformly continuous on s.

theorem UniformContinuousOn.inv₀ {α : Type u_1} [NormedDivisionRing α] {X : Type u_4} [UniformSpace X] {f : X → α} {s : Set X} (hf : UniformContinuousOn f s) (hf₀ : (f '' s)ᶜ ∈ nhds 0) : UniformContinuousOn f⁻¹ s

theorem UniformContinuousOn.fun_inv₀ {α : Type u_1} [NormedDivisionRing α] {X : Type u_4} [UniformSpace X] {f : X → α} {s : Set X} (hf : UniformContinuousOn f s) (hf₀ : (f '' s)ᶜ ∈ nhds 0) : UniformContinuousOn (fun (i : X) => (f i)⁻¹) s

Eta-expanded form of UniformContinuousOn.inv₀

theorem UniformContinuous.inv₀ {α : Type u_1} [NormedDivisionRing α] {X : Type u_4} [UniformSpace X] {f : X → α} (hf : UniformContinuous f) (hf₀ : (Set.range f)ᶜ ∈ nhds 0) : UniformContinuous f⁻¹

theorem UniformContinuous.fun_inv₀ {α : Type u_1} [NormedDivisionRing α] {X : Type u_4} [UniformSpace X] {f : X → α} (hf : UniformContinuous f) (hf₀ : (Set.range f)ᶜ ∈ nhds 0) : UniformContinuous fun (i : X) => (f i)⁻¹

Eta-expanded form of UniformContinuous.inv₀

theorem TendstoLocallyUniformlyOn.inv₀_of_disjoint {α : Type u_1} [NormedDivisionRing α] {X : Type u_4} {ι : Type u_5} [TopologicalSpace X] {s : Set X} {F : ι → X → α} {f : X → α} {l : Filter ι} (hF : TendstoLocallyUniformlyOn F f l s) (hf : ∀ x ∈ s, Disjoint (Filter.map f (nhdsWithin x s)) (nhds 0)) : TendstoLocallyUniformlyOn F⁻¹ f⁻¹ l s

theorem TendstoLocallyUniformlyOn.fun_inv₀_of_disjoint {α : Type u_1} [NormedDivisionRing α] {X : Type u_4} {ι : Type u_5} [TopologicalSpace X] {s : Set X} {F : ι → X → α} {f : X → α} {l : Filter ι} (hF : TendstoLocallyUniformlyOn F f l s) (hf : ∀ x ∈ s, Disjoint (Filter.map f (nhdsWithin x s)) (nhds 0)) : TendstoLocallyUniformlyOn (fun (i : ι) (i_1 : X) => (F i i_1)⁻¹) (fun (i : X) => (f i)⁻¹) l s

Eta-expanded form of TendstoLocallyUniformlyOn.inv₀_of_disjoint

theorem TendstoLocallyUniformly.inv₀_of_disjoint {α : Type u_1} [NormedDivisionRing α] {X : Type u_4} {ι : Type u_5} [TopologicalSpace X] {F : ι → X → α} {f : X → α} {l : Filter ι} (hF : TendstoLocallyUniformly F f l) (hf : ∀ (x : X), Disjoint (Filter.map f (nhds x)) (nhds 0)) : TendstoLocallyUniformly F⁻¹ f⁻¹ l

theorem TendstoLocallyUniformly.fun_inv₀_of_disjoint {α : Type u_1} [NormedDivisionRing α] {X : Type u_4} {ι : Type u_5} [TopologicalSpace X] {F : ι → X → α} {f : X → α} {l : Filter ι} (hF : TendstoLocallyUniformly F f l) (hf : ∀ (x : X), Disjoint (Filter.map f (nhds x)) (nhds 0)) : TendstoLocallyUniformly (fun (i : ι) (i_1 : X) => (F i i_1)⁻¹) (fun (i : X) => (f i)⁻¹) l

Eta-expanded form of TendstoLocallyUniformly.inv₀_of_disjoint

theorem TendstoLocallyUniformlyOn.inv₀ {α : Type u_1} [NormedDivisionRing α] {X : Type u_4} {ι : Type u_5} [TopologicalSpace X] {s : Set X} {F : ι → X → α} {f : X → α} {l : Filter ι} (hF : TendstoLocallyUniformlyOn F f l s) (hf : ContinuousOn f s) (hf₀ : ∀ x ∈ s, f x ≠ 0) : TendstoLocallyUniformlyOn F⁻¹ f⁻¹ l s

theorem TendstoLocallyUniformlyOn.fun_inv₀ {α : Type u_1} [NormedDivisionRing α] {X : Type u_4} {ι : Type u_5} [TopologicalSpace X] {s : Set X} {F : ι → X → α} {f : X → α} {l : Filter ι} (hF : TendstoLocallyUniformlyOn F f l s) (hf : ContinuousOn f s) (hf₀ : ∀ x ∈ s, f x ≠ 0) : TendstoLocallyUniformlyOn (fun (i : ι) (i_1 : X) => (F i i_1)⁻¹) (fun (i : X) => (f i)⁻¹) l s

Eta-expanded form of TendstoLocallyUniformlyOn.inv₀

theorem TendstoLocallyUniformly.inv₀ {α : Type u_1} [NormedDivisionRing α] {X : Type u_4} {ι : Type u_5} [TopologicalSpace X] {F : ι → X → α} {f : X → α} {l : Filter ι} (hF : TendstoLocallyUniformly F f l) (hf : Continuous f) (hf₀ : ∀ (x : X), f x ≠ 0) : TendstoLocallyUniformly F⁻¹ f⁻¹ l

theorem TendstoLocallyUniformly.fun_inv₀ {α : Type u_1} [NormedDivisionRing α] {X : Type u_4} {ι : Type u_5} [TopologicalSpace X] {F : ι → X → α} {f : X → α} {l : Filter ι} (hF : TendstoLocallyUniformly F f l) (hf : Continuous f) (hf₀ : ∀ (x : X), f x ≠ 0) : TendstoLocallyUniformly (fun (i : ι) (i_1 : X) => (F i i_1)⁻¹) (fun (i : X) => (f i)⁻¹) l

Eta-expanded form of TendstoLocallyUniformly.inv₀

@[instance 100]

instance NormedDivisionRing.to_continuousInv₀ {α : Type u_1} [NormedDivisionRing α] : ContinuousInv₀ α

@[deprecated NormedDivisionRing.to_continuousInv₀ (since := "2025-09-01")]

theorem NormedDivisionRing.to_hasContinuousInv₀ {α : Type u_1} [NormedDivisionRing α] : ContinuousInv₀ α

Alias of NormedDivisionRing.to_continuousInv₀.

theorem TendstoLocallyUniformlyOn.div₀ {α : Type u_1} [NormedDivisionRing α] {X : Type u_4} {ι : Type u_5} [TopologicalSpace X] {s : Set X} {F G : ι → X → α} {f g : X → α} {l : Filter ι} (hF : TendstoLocallyUniformlyOn F f l s) (hG : TendstoLocallyUniformlyOn G g l s) (hf : ContinuousOn f s) (hg : ContinuousOn g s) (hg₀ : ∀ x ∈ s, g x ≠ 0) : TendstoLocallyUniformlyOn (F / G) (f / g) l s

theorem TendstoLocallyUniformlyOn.fun_div₀ {α : Type u_1} [NormedDivisionRing α] {X : Type u_4} {ι : Type u_5} [TopologicalSpace X] {s : Set X} {F G : ι → X → α} {f g : X → α} {l : Filter ι} (hF : TendstoLocallyUniformlyOn F f l s) (hG : TendstoLocallyUniformlyOn G g l s) (hf : ContinuousOn f s) (hg : ContinuousOn g s) (hg₀ : ∀ x ∈ s, g x ≠ 0) : TendstoLocallyUniformlyOn (fun (i : ι) (i_1 : X) => F i i_1 / G i i_1) (fun (i : X) => f i / g i) l s

Eta-expanded form of TendstoLocallyUniformlyOn.div₀

theorem TendstoLocallyUniformly.div₀ {α : Type u_1} [NormedDivisionRing α] {X : Type u_4} {ι : Type u_5} [TopologicalSpace X] {F G : ι → X → α} {f g : X → α} {l : Filter ι} (hF : TendstoLocallyUniformly F f l) (hG : TendstoLocallyUniformly G g l) (hf : Continuous f) (hg : Continuous g) (hg₀ : ∀ (x : X), g x ≠ 0) : TendstoLocallyUniformly (F / G) (f / g) l

theorem TendstoLocallyUniformly.fun_div₀ {α : Type u_1} [NormedDivisionRing α] {X : Type u_4} {ι : Type u_5} [TopologicalSpace X] {F G : ι → X → α} {f g : X → α} {l : Filter ι} (hF : TendstoLocallyUniformly F f l) (hG : TendstoLocallyUniformly G g l) (hf : Continuous f) (hg : Continuous g) (hg₀ : ∀ (x : X), g x ≠ 0) : TendstoLocallyUniformly (fun (i : ι) (i_1 : X) => F i i_1 / G i i_1) (fun (i : X) => f i / g i) l

Eta-expanded form of TendstoLocallyUniformly.div₀

@[instance 100]

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

A normed division ring is a topological division ring.

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

@[deprecated tendsto_norm_inv_nhdsNE_zero_atTop (since := "2025-11-26")]

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

Alias of tendsto_norm_inv_nhdsNE_zero_atTop.

theorem tendsto_zpow_nhdsNE_zero_cobounded {α : Type u_1} [NormedDivisionRing α] {m : ℤ} (hm : m < 0) : Filter.Tendsto (fun (x : α) => x ^ m) (nhdsWithin 0 {0}ᶜ) (Bornology.cobounded α)

@[deprecated tendsto_zpow_nhdsNE_zero_cobounded (since := "2025-11-26")]

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

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)