instIsTopologicalDivisionRing — Mathlib

English

The completion hat K is a topological division ring, i.e., it has a compatible topology and division ring operations.

Русский

Дополнение hat K является топологическим делением кольца: есть совместная топология и операции деления.

LaTeX

$$$\text{IsTopologicalDivisionRing}(\hat K)$$$

Lean4

instance : IsTopologicalDivisionRing (hat K) :=
  { Completion.topologicalRing with
    continuousAt_inv₀ := by
      intro x x_ne
      have : {y | hatInv y = y⁻¹} ∈ 𝓝 x :=
        haveI : {(0 : hat K)}ᶜ ⊆ {y : hat K | hatInv y = y⁻¹} :=
          by
          intro y y_ne
          rw [mem_compl_singleton_iff] at y_ne
          dsimp [Inv.inv]
          rw [if_neg y_ne]
        mem_of_superset (compl_singleton_mem_nhds x_ne) this
      exact ContinuousAt.congr (continuous_hatInv x_ne) this }

Похожие утверждения