The category of additive commutative groups is preadditive.

instance AddCommGroupCat.instAddCommGroupHomAddCommGroupCatToQuiverToCategoryStructInstAddCommGroupCatLargeCategory (P : AddCommGroupCat) (Q : AddCommGroupCat) : AddCommGroup (P ⟶ Q)

@[simp]

theorem AddCommGroupCat.hom_add_apply {P : AddCommGroupCat} {Q : AddCommGroupCat} (f : P ⟶ Q) (g : P ⟶ Q) (x : ↑P) : ↑(f + g) x = ↑f x + ↑g x

instance AddCommGroupCat.instPreadditiveAddCommGroupCatInstAddCommGroupCatLargeCategory : CategoryTheory.Preadditive AddCommGroupCat