Commit 2024-02-24 21:34 13ae635b

View on Github →

feat(CategoryTheory/Monoidal/Mon_): add simp lemmas (#10905)

Estimated changes

Modified Mathlib/CategoryTheory/Monoidal/Mon_.lean

added theorem Mon_.associator_hom_hom

added theorem Mon_.associator_inv_hom

added theorem Mon_.leftUnitor_hom_hom

added theorem Mon_.leftUnitor_inv_hom

added theorem Mon_.rightUnitor_hom_hom

added theorem Mon_.rightUnitor_inv_hom

added theorem Mon_.tensorUnit_X

added theorem Mon_.whiskerLeft_hom

added theorem Mon_.whiskerRight_hom