# mathlibdocumentation

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.

@[protected, instance]
@[protected, instance]
@[protected, instance]
@[protected, instance]