Documentation

Mathlib.Algebra.Category.Grp.Preadditive

The category of additive commutative groups is preadditive. #

@[simp]
theorem AddCommGrp.hom_add {M N : AddCommGrp} (f g : M N) :
@[simp]
@[simp]
theorem AddCommGrp.hom_nsmul {M N : AddCommGrp} (n : ) (f : M N) :
@[simp]
theorem AddCommGrp.hom_neg {M N : AddCommGrp} (f : M N) :
@[simp]
theorem AddCommGrp.hom_sub {M N : AddCommGrp} (f g : M N) :
@[simp]
theorem AddCommGrp.hom_zsmul {M N : AddCommGrp} (n : ) (f : M N) :

AddCommGrp.Hom.hom bundled as an additive equivalence.

Equations
Instances For