Commit 2023-08-01 12:02 881c6469

View on Github →

chore: cleanup API for distributors in preadditive monoidal categories (#6257)

Estimated changes

Modified Mathlib/CategoryTheory/Monoidal/Preadditive.lean

added theorem CategoryTheory.biproduct_ι_comp_leftDistributor_hom

added theorem CategoryTheory.biproduct_ι_comp_leftDistributor_inv

added theorem CategoryTheory.biproduct_ι_comp_rightDistributor_hom

added theorem CategoryTheory.biproduct_ι_comp_rightDistributor_inv

added theorem CategoryTheory.leftDistributor_ext_left

added theorem CategoryTheory.leftDistributor_ext_right

added theorem CategoryTheory.leftDistributor_ext₂_left

added theorem CategoryTheory.leftDistributor_ext₂_right

added theorem CategoryTheory.leftDistributor_hom_comp_biproduct_π

added theorem CategoryTheory.leftDistributor_inv_comp_biproduct_π

modified theorem CategoryTheory.leftDistributor_rightDistributor_assoc

modified def CategoryTheory.rightDistributor

modified theorem CategoryTheory.rightDistributor_assoc

added theorem CategoryTheory.rightDistributor_ext_left

added theorem CategoryTheory.rightDistributor_ext_right

added theorem CategoryTheory.rightDistributor_ext₂_left

added theorem CategoryTheory.rightDistributor_ext₂_right

modified theorem CategoryTheory.rightDistributor_hom

added theorem CategoryTheory.rightDistributor_hom_comp_biproduct_π

modified theorem CategoryTheory.rightDistributor_inv

added theorem CategoryTheory.rightDistributor_inv_comp_biproduct_π