English
There is a canonical way to regard any group M as an object of GrpCat by bundling its underlying type with its group structure.
Русский
Существует канонический способ рассмотреть любую группу M как объект GrpCat, объединив её множественный тип с групповой структурой.
LaTeX
$$$\GrpCat.of(M) = \langle M \rangle \text{ with the given group structure on } M.$$$
Lean4
/-- Construct a bundled `GrpCat` from the underlying type and typeclass. -/
@[to_additive /-- Construct a bundled `AddGrpCat` from the underlying type and typeclass. -/
]
abbrev of (M : Type u) [Group M] : GrpCat :=
⟨M⟩