instHasForget₂FiniteGrp — Mathlib

English

From a profinite group G, equipped with its topology, there is a canonical ProfiniteGroup structure on G.

Русский

Из профинитной группы G, оснащённой соответствующей топологией, получается каноническая структура ProfiniteGrp на G.

LaTeX

$$$\operatorname{ProfiniteGrp.ofProfinite}(G) = \operatorname{ProfiniteGrp.of}(G)$$$

Lean4

@[to_additive]
instance : HasForget₂ FiniteGrp ProfiniteGrp where
  forget₂ :=
    { obj := ofFiniteGrp
      map := fun f => ⟨f.hom, by continuity⟩ }

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