The category of abelian groups is abelian

@[implicit_reducible]

noncomputable def AddCommGrpCat.normalMono {X Y : AddCommGrpCat} (f : X ⟶ Y) : CategoryTheory.Mono f → CategoryTheory.NormalMono f

In the category of abelian groups, every monomorphism is normal.

@[implicit_reducible]

noncomputable def AddCommGrpCat.normalEpi {X Y : AddCommGrpCat} (f : X ⟶ Y) : CategoryTheory.Epi f → CategoryTheory.NormalEpi f

In the category of abelian groups, every epimorphism is normal.

@[implicit_reducible]

instance AddCommGrpCat.instAbelian : CategoryTheory.Abelian AddCommGrpCat

The category of abelian groups is abelian.