English
The topology on a division ring arising from a valuation turns it into a topological division ring.
Русский
топология, порожденная валюацией на делении кольцо превращает его в топологическое деление кольцо.
LaTeX
$$$IsTopologicalDivisionRing(K)$$$
Lean4
/-- The topology coming from a valuation on a division ring makes it a topological division ring
[BouAC, VI.5.1 middle of Proposition 1] -/
instance (priority := 100) isTopologicalDivisionRing [Valued K Γ₀] : IsTopologicalDivisionRing K :=
{ (by infer_instance : IsTopologicalRing K) with
continuousAt_inv₀ := by
intro x x_ne s s_in
obtain ⟨γ, hs⟩ := Valued.mem_nhds.mp s_in; clear s_in
rw [mem_map, Valued.mem_nhds]
change ∃ γ : Γ₀ˣ, {y : K | (v (y - x) : Γ₀) < γ} ⊆ {x : K | x⁻¹ ∈ s}
have vx_ne := (Valuation.ne_zero_iff <| v).mpr x_ne
let γ' := Units.mk0 _ vx_ne
use min (γ * (γ' * γ')) γ'
intro y y_in
apply hs
simp only [mem_setOf_eq] at y_in
rw [Units.min_val, Units.val_mul, Units.val_mul] at y_in
exact Valuation.inversion_estimate _ x_ne y_in }
