instIsTopologicalGroupMultiplicativeOfIsTopologicalAddGroup

English

If G is an additive topological group, then the multiplicative version of G, denoted Multiplicative G, is a topological group.

Русский

Если G — аддитивная топологическая группа, то мультипликативная версия G является топологической группой.

LaTeX

$$$ IsTopologicalGroup (Multiplicative G) $$$

Lean4

instance {G} [TopologicalSpace G] [AddGroup G] [IsTopologicalAddGroup G] : IsTopologicalGroup (Multiplicative G) where
  continuous_inv := @continuous_neg G _ _ _

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