The category of additive commutative groups is preadditive.

instance AddCommGrp.instAddCommGroupHom (P Q : AddCommGrp) : AddCommGroup (P ⟶ Q)

Equations

• P.instAddCommGroupHom Q = inferInstance

@[simp]

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

instance AddCommGrp.instPreadditive : CategoryTheory.Preadditive AddCommGrp

Equations

• AddCommGrp.instPreadditive = { homGroup := inferInstance, add_comp := AddCommGrp.instPreadditive.proof_1, comp_add := AddCommGrp.instPreadditive.proof_2 }