The category of additive commutative groups is preadditive. #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.
@[protected, 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}