English
For X in ModuleCat R, the forget₂-object equals the additive-commutative-group object with carrier X.
Русский
Для X в ModuleCat R объект forget₂ равен объекту AddCommGrpCat с носителем X.
LaTeX
$$$ (\mathsf{forget}_2\;\mathrm{ModuleCat}\; R).\mathrm{obj} X = \mathrm{AddCommGrpCat}.of X \;\text{(carrier } X\text{)} $$$
Lean4
@[scoped macro ModuleCat.«term↟_»]
public meta def «_aux_Mathlib_Algebra_Category_ModuleCat_Basic___macroRules_ModuleCat_term↟__1» : Macro✝ := fun
| `(↟$f) => ``(ModuleCat.ofHom $f)
| _ => no_error_if_unused% throw✝ Lean.Macro.Exception.unsupportedSyntax✝
