English
There is a canonical way to form a FiniteGrp from a type G with a finite group structure: toGrp is GrpCat.of G and isFinite is the given finiteness.
Русский
Существует канонический способ получить FiniteGrp из типа G, на котором задана конечная группа: toGrp равно GrpCat.of G, а isFinite задано.
LaTeX
$$$$ \text{FiniteGrp.of}(G) \text{ is a finite group object with } \text{toGrp} = \mathrm{GrpCat.of}(G) \text{ and } \text{isFinite} = \text{inst} \,$$$$
Lean4
/-- Construct a term of `FiniteGrp` from a type endowed with the structure of a finite group. -/
@[to_additive /-- Construct a term of `FiniteAddGrp` from a type endowed with the structure of a
finite additive group. -/
]
def of (G : Type u) [Group G] [Finite G] : FiniteGrp
where
toGrp := GrpCat.of G
isFinite := ‹_›
