Mathlib Changelog
v4
Changelog
About
Github
Commit
2023-05-29 14:57
5f0e28cc
View on Github →
feat: port CategoryTheory.Monoidal.CoherenceLemmas (
#4359
)
depends on:
#4357
Estimated changes
Modified
Mathlib.lean
Created
Mathlib/CategoryTheory/Monoidal/CoherenceLemmas.lean
added
theorem
CategoryTheory.MonoidalCategory.id_tensor_rightUnitor_inv
added
theorem
CategoryTheory.MonoidalCategory.leftUnitor_inv_tensor_id
added
theorem
CategoryTheory.MonoidalCategory.leftUnitor_tensor'
added
theorem
CategoryTheory.MonoidalCategory.leftUnitor_tensor
added
theorem
CategoryTheory.MonoidalCategory.leftUnitor_tensor_inv
added
theorem
CategoryTheory.MonoidalCategory.pentagon_hom_inv
added
theorem
CategoryTheory.MonoidalCategory.pentagon_inv_hom
added
theorem
CategoryTheory.MonoidalCategory.pentagon_inv_inv_hom
added
theorem
CategoryTheory.MonoidalCategory.triangle_assoc_comp_right_inv
added
theorem
CategoryTheory.MonoidalCategory.unitors_equal
added
theorem
CategoryTheory.MonoidalCategory.unitors_inv_equal