Documentation

Mathlib.Algebra.Category.Grp.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.