Theorem CategoryTheory.MonoidalCategory.leftUnitor_tensor'

Modification history

2025-06-27 10:00

Mathlib/CategoryTheory/Monoidal/CoherenceLemmas.lean

chore(CategoryTheory/Monoidal): fix a few lemma names (#26256) …

Deleted CategoryTheory.MonoidalCategory.leftUnitor_tensor'View on Github →

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'View on Github →

2024-01-31 07:01

Mathlib/CategoryTheory/Monoidal/Category.lean

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

Modified CategoryTheory.MonoidalCategory.leftUnitor_tensor'View on Github →

2023-05-29 14:57

Mathlib/CategoryTheory/Monoidal/CoherenceLemmas.lean

feat: port CategoryTheory.Monoidal.CoherenceLemmas (#4359) …

Added CategoryTheory.MonoidalCategory.leftUnitor_tensor'View on Github →