instGroup — Mathlib

English

If G is a Group with IsTopologicalGroup, then SeparationQuotient G forms a Group (redundant but parallel to prior).

Русский

Если G — группа с IsTopologicalGroup, SeparationQuotient G образует группу.

LaTeX

$$$\operatorname{Group}(\mathrm{SeparationQuotient}(G))$$$

Lean4

@[to_additive]
instance instGroup [Group G] [IsTopologicalGroup G] : Group (SeparationQuotient G) :=
  surjective_mk.group mk mk_one mk_mul mk_inv mk_div mk_pow mk_zpow

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