ofProfinite — Mathlib

English

From a profinite type G, the construction of a ProfiniteGrp yields a profinite topological group.

Русский

Из профинитного типа G строится топологическая группа профинитного типа.

LaTeX

$$$ \text{ProfiniteGrp}.ofProfinite(G) $ is a ProfiniteGrp$$

Lean4

/-- Construct a term of `ProfiniteGrp` from a type endowed with the structure of a
profinite topological group. -/
@[to_additive /-- Construct a term of `ProfiniteAddGrp` from a type endowed with the structure of a
    profinite topological additive group. -/
    ]
abbrev ofProfinite (G : Profinite) [Group G] [IsTopologicalGroup G] : ProfiniteGrp :=
  of G

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