Commit 2023-03-22 13:29 071e0bfe

View on Github →

feat: port CategoryTheory.Monoidal.Preadditive (#3033)

Estimated changes

Modified Mathlib.lean

Created Mathlib/CategoryTheory/Monoidal/Preadditive.lean

added def CategoryTheory.leftDistributor

added theorem CategoryTheory.leftDistributor_assoc

added theorem CategoryTheory.leftDistributor_hom

added theorem CategoryTheory.leftDistributor_inv

added theorem CategoryTheory.leftDistributor_rightDistributor_assoc

added theorem CategoryTheory.monoidalPreadditive_of_faithful

added def CategoryTheory.rightDistributor

added theorem CategoryTheory.rightDistributor_assoc

added theorem CategoryTheory.rightDistributor_hom

added theorem CategoryTheory.rightDistributor_inv

added theorem CategoryTheory.sum_tensor

added theorem CategoryTheory.tensor_sum