The category of (commutative) (additive) groups has a zero object. #
AddCommGroup
also has zero morphisms. For definitional reasons, we infer this from preadditivity
rather than from the existence of a zero object.
Mathlib.Algebra.Category.GroupCat.Zero
AddCommGroup
also has zero morphisms. For definitional reasons, we infer this from preadditivity
rather than from the existence of a zero object.