# 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`

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_symm_apply {α : Type u_1} [NormedDivisionRing α] (a : α) (ha : a ≠ 0) (x : α) :
(mulLeft a ha).symm x = a⁻¹ * x
source
@[simp]
theorem DilationEquiv.mulLeft_apply {α : Type u_1} [NormedDivisionRing α] (a : α) (ha : a ≠ 0) (x : α) :
(mulLeft a ha) 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_symm_apply {α : Type u_1} [NormedDivisionRing α] (a : α) (ha : a ≠ 0) (x : α) :
(mulRight a ha).symm x = x * a⁻¹
source
@[simp]
theorem DilationEquiv.mulRight_apply {α : Type u_1} [NormedDivisionRing α] (a : α) (ha : a ≠ 0) (x : α) :
(mulRight a ha) 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_continuousInv₀ {α : Type u_1} [NormedDivisionRing α] :
ContinuousInv₀ α
source
@[deprecated NormedDivisionRing.to_continuousInv₀ (since := "2025-09-01")]
theorem NormedDivisionRing.to_hasContinuousInv₀ {α : Type u_1} [NormedDivisionRing α] :
ContinuousInv₀ α

Alias of `NormedDivisionRing.to_continuousInv₀`.

source
@[instance 100]
instance NormedDivisionRing.to_isTopologicalDivisionRing {α : Type u_1} [NormedDivisionRing α] :
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
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
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.

source
theorem NormedField.discreteTopology_of_bddAbove_range_norm {𝕜 : Type u_4} [NormedField 𝕜] (h : BddAbove (Set.range fun (k : 𝕜) => ‖k‖)) :
DiscreteTopology 𝕜
source
theorem NormedField.denseRange_nnnorm (α : Type u_1) [DenselyNormedField α] :
DenseRange nnnorm
source
@[simp]
theorem NormedField.continuousAt_zpow {𝕜 : Type u_4} [NontriviallyNormedField 𝕜] {n : ℤ} {x : 𝕜} :
ContinuousAt (fun (x : 𝕜) => x ^ n) x ↔ x ≠ 0 ∨ 0 ≤ n
source
@[simp]
theorem NormedField.continuousAt_inv {𝕜 : Type u_4} [NontriviallyNormedField 𝕜] {x : 𝕜} :
ContinuousAt Inv.inv x ↔ x ≠ 0
source
instance Rat.instNormedField :
NormedField ℚ
Equations

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

source
instance Rat.instDenselyNormedField :
DenselyNormedField ℚ
Equations

- Rat.instDenselyNormedField = { toNormedField := Rat.instNormedField, lt_norm_lt := Rat.instDenselyNormedField._proof_1 }

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