mathlib documentation

algebra.category.Group.zero

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.