Documentation

Mathlib.Algebra.Category.GroupCat.Preadditive

The category of additive commutative groups is preadditive. #

Equations
  • P.instAddCommGroupHom Q = inferInstance
@[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