Commit 2023-03-09 16:23 44e69b99

View on Github →

feat: port CategoryTheory.Abelian.NonPreadditive (#2752)

Estimated changes

Modified Mathlib.lean

Created Mathlib/CategoryTheory/Abelian/NonPreadditive.lean

added theorem CategoryTheory.NonPreadditiveAbelian.add_assoc

added theorem CategoryTheory.NonPreadditiveAbelian.add_comm

added theorem CategoryTheory.NonPreadditiveAbelian.add_comp

added theorem CategoryTheory.NonPreadditiveAbelian.add_def

added theorem CategoryTheory.NonPreadditiveAbelian.add_neg

added theorem CategoryTheory.NonPreadditiveAbelian.add_neg_self

added theorem CategoryTheory.NonPreadditiveAbelian.add_zero

added theorem CategoryTheory.NonPreadditiveAbelian.comp_add

added theorem CategoryTheory.NonPreadditiveAbelian.comp_sub

added theorem CategoryTheory.NonPreadditiveAbelian.diag_σ

added def CategoryTheory.NonPreadditiveAbelian.epiIsCokernelOfKernel

added def CategoryTheory.NonPreadditiveAbelian.hasAdd

added def CategoryTheory.NonPreadditiveAbelian.hasNeg

added def CategoryTheory.NonPreadditiveAbelian.hasSub

added def CategoryTheory.NonPreadditiveAbelian.isColimitσ

added theorem CategoryTheory.NonPreadditiveAbelian.lift_map

added theorem CategoryTheory.NonPreadditiveAbelian.lift_sub_lift

added theorem CategoryTheory.NonPreadditiveAbelian.lift_σ

added def CategoryTheory.NonPreadditiveAbelian.monoIsKernelOfCokernel

added theorem CategoryTheory.NonPreadditiveAbelian.neg_add

added theorem CategoryTheory.NonPreadditiveAbelian.neg_add_self

added theorem CategoryTheory.NonPreadditiveAbelian.neg_def

added theorem CategoryTheory.NonPreadditiveAbelian.neg_neg

added theorem CategoryTheory.NonPreadditiveAbelian.neg_sub'

added theorem CategoryTheory.NonPreadditiveAbelian.neg_sub

added def CategoryTheory.NonPreadditiveAbelian.preadditive

added theorem CategoryTheory.NonPreadditiveAbelian.sub_add

added theorem CategoryTheory.NonPreadditiveAbelian.sub_comp

added theorem CategoryTheory.NonPreadditiveAbelian.sub_def

added theorem CategoryTheory.NonPreadditiveAbelian.sub_self

added theorem CategoryTheory.NonPreadditiveAbelian.sub_sub_sub

added theorem CategoryTheory.NonPreadditiveAbelian.sub_zero

added theorem CategoryTheory.NonPreadditiveAbelian.σ_comp