English
Typecheck a MonoidHom as a morphism in CommGrpCat; i.e., given f : X →* Y with CommGroup structures, there is a corresponding morphism in CommGrpCat from X to Y.
Русский
Типизация MonoidHom как морфизма в CommGrpCat; дано f: X →* Y с структурой CommGroup, существует соответствующий морфизм в CommGrpCat от X к Y.
LaTeX
$$$ \\text{ofHom } f : \\mathrm{of}\,X \\to \\mathrm{of}\,Y $$$
Lean4
/-- Typecheck a `MonoidHom` as a morphism in `CommGrpCat`. -/
@[to_additive /-- Typecheck an `AddMonoidHom` as a morphism in `AddCommGrpCat`. -/
]
abbrev ofHom {X Y : Type u} [CommGroup X] [CommGroup Y] (f : X →* Y) : of X ⟶ of Y :=
ConcreteCategory.ofHom (C := CommGrpCat) f
