Def CategoryTheory.MonoidalCategory.tensorUnitLeft

Modification history

2024-05-15 10:47

Mathlib/CategoryTheory/Monoidal/Category.lean

feat(CategoryTheory/Monoidal): the curried associator isomorphism (#11701) …

Deleted CategoryTheory.MonoidalCategory.tensorUnitLeft View on Github →

2023-02-18 19:03

Mathlib/CategoryTheory/Monoidal/Category.lean

feat: port CategoryTheory.Monoidal.Category (#2318)

Added CategoryTheory.MonoidalCategory.tensorUnitLeft View on Github →