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:

source

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' := ⋯ }

Instances For

source

@[simp]

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

(mulLeft a ha) x = a * x

source

@[simp]

theorem DilationEquiv.mulLeft_symm_apply {α : Type u_1} [NormedDivisionRing α] (a : α) (ha : a ≠ 0) (x : α) :

(mulLeft a ha).symm x = a⁻¹ * x

source

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' := ⋯ }

Instances For

source

@[simp]

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

(mulRight a ha) x = x * a

source

@[simp]

theorem DilationEquiv.mulRight_symm_apply {α : Type u_1} [NormedDivisionRing α] (a : α) (ha : a ≠ 0) (x : α) :

(mulRight a ha).symm x = x * a⁻¹

source

@[simp]

theorem Filter.map_mul_left_cobounded {α : Type u_1} [NormedDivisionRing α] {a : α} (ha : a ≠ 0) :

map (fun (x : α) => a * x) (Bornology.cobounded α) = Bornology.cobounded α

source

@[simp]

theorem Filter.map_mul_right_cobounded {α : Type u_1} [NormedDivisionRing α] {a : α} (ha : a ≠ 0) :

map (fun (x : α) => x * a) (Bornology.cobounded α) = Bornology.cobounded α

source

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.

source

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.

source

@[simp]

theorem Filter.inv_cobounded₀ {α : Type u_1} [NormedDivisionRing α] :

(Bornology.cobounded α)⁻¹ = nhdsWithin 0 {0}ᶜ

source

@[simp]

theorem Filter.inv_nhdsWithin_ne_zero {α : Type u_1} [NormedDivisionRing α] :

(nhdsWithin 0 {0}ᶜ)⁻¹ = Bornology.cobounded α

source

theorem Filter.tendsto_inv₀_cobounded' {α : Type u_1} [NormedDivisionRing α] :

Tendsto Inv.inv (Bornology.cobounded α) (nhdsWithin 0 {0}ᶜ)

source

theorem Filter.tendsto_inv₀_cobounded {α : Type u_1} [NormedDivisionRing α] :

Tendsto Inv.inv (Bornology.cobounded α) (nhds 0)

source

theorem Filter.tendsto_inv₀_nhdsWithin_ne_zero {α : Type u_1} [NormedDivisionRing α] :

Tendsto Inv.inv (nhdsWithin 0 {0}ᶜ) (Bornology.cobounded α)

source

@[instance 100]

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

HasContinuousInv₀ α

source

@[instance 100]

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

IsTopologicalDivisionRing α

A normed division ring is a topological division ring.

source

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

source

theorem NormedField.tendsto_norm_inv_nhdsNE_zero_atTop {α : Type u_1} [NormedDivisionRing α] :

Filter.Tendsto (fun (x : α) => ‖x⁻¹ ‖) (nhdsWithin 0 {0}ᶜ) Filter.atTop

source

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

source

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

source

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

source

theorem NormedField.discreteTopology_or_nontriviallyNormedField (𝕜 : Type u_4) [h : NormedField 𝕜] :

DiscreteTopology 𝕜 ∨ Nonempty { h' : NontriviallyNormedField 𝕜 // NontriviallyNormedField.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.

source