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