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.

@[instance]

@[instance]

Equations
@[instance]

Equations