The category of additive commutative groups is preadditive.
@[instance]
Equations
- AddCommGroup.category_theory.preadditive = {hom_group := λ (P Q : AddCommGroup), add_monoid_hom.add_comm_group, add_comp' := AddCommGroup.category_theory.preadditive._proof_1, comp_add' := AddCommGroup.category_theory.preadditive._proof_2}