Commit 2023-03-17 12:26 d2cf8db8

View on Github →

feat: port CategoryTheory.Preadditive.OfBiproducts (#2939)

Estimated changes

Modified Mathlib.lean

Created Mathlib/CategoryTheory/Preadditive/OfBiproducts.lean

added def CategoryTheory.SemiadditiveOfBinaryBiproducts.addCommMonoidHomOfHasBinaryBiproducts

added theorem CategoryTheory.SemiadditiveOfBinaryBiproducts.add_comp

added theorem CategoryTheory.SemiadditiveOfBinaryBiproducts.add_eq_left_addition

added theorem CategoryTheory.SemiadditiveOfBinaryBiproducts.add_eq_right_addition

added theorem CategoryTheory.SemiadditiveOfBinaryBiproducts.comp_add

added theorem CategoryTheory.SemiadditiveOfBinaryBiproducts.distrib

added theorem CategoryTheory.SemiadditiveOfBinaryBiproducts.isUnital_leftAdd

added theorem CategoryTheory.SemiadditiveOfBinaryBiproducts.isUnital_rightAdd

added def CategoryTheory.SemiadditiveOfBinaryBiproducts.leftAdd

added def CategoryTheory.SemiadditiveOfBinaryBiproducts.rightAdd