instIsTopologicalDivisionRing — Mathlib

English

If K is a nonarchimedean local field, then K is a topological division ring (in particular, a topological field).

Русский

Если K — неархимедово локальное поле, то K является топологическим делимым кольцом (то есть топологическим полем).

LaTeX

$$$$K ext{ is a topological division ring}.$$$$

Lean4

instance : IsTopologicalDivisionRing K :=
  by
  letI := IsTopologicalAddGroup.toUniformSpace K
  haveI := isUniformAddGroup_of_addCommGroup (G := K)
  infer_instance

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