The category of additive commutative groups is preadditive.

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

Equations

• P.instAddCommGroupHom Q = inferInstance

@[simp]

theorem AddCommGrp.hom_add_apply {P : AddCommGrp} {Q : AddCommGrp} (f : P ⟶ Q) (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 }