Theorem CategoryTheory.MonoidalCategory.leftUnitor_inv_naturality'

Modification history

2024-03-01 18:37

Mathlib/CategoryTheory/Monoidal/Category.lean

feat(CategoryTheory/Monoidal): replace `𝟙 X ⊗ f` with `X ◁ f` (#10912) …

Deleted CategoryTheory.MonoidalCategory.leftUnitor_inv_naturality'View on Github →

2024-01-31 07:01

Mathlib/CategoryTheory/Monoidal/Category.lean

feat(CategoryTheory/Monoidal): partially setting simp lemmas (#10061) …

Added CategoryTheory.MonoidalCategory.leftUnitor_inv_naturality'View on Github →