instIsTopologicalGroupOfContinuousMul

English

If α is a monoid with continuous multiplication, then the unit group αˣ is a topological group.

Русский

Если α — моноид с непрерывным умножением, то группа единиц αˣ является топологической группой.

LaTeX

$$$ IsTopologicalGroup (\\alpha^{\\times}) $$$

Lean4

@[to_additive]
instance [ContinuousMul α] : IsTopologicalGroup αˣ where
  continuous_inv := Units.continuous_iff.2 <| ⟨continuous_coe_inv, continuous_val⟩

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