Theorem CategoryTheory.MonoidalCategory.leftUnitor_tensor_inv'

Modification history

2024-03-01 18:37

Mathlib/CategoryTheory/Monoidal/Category.lean

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

Modified CategoryTheory.MonoidalCategory.leftUnitor_tensor_inv'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_tensor_inv'View on Github →