Mathlib v3 is deprecated. Go to Mathlib v4

Theorem category_theory.monoidal_category.left_unitor_conjugation

Modification history

2020-10-15 07:30
src/category_theory/monoidal/category.lean
chore(category_theory/monoidal): fix typo in docstrings (#4625)
Modified category_theory.monoidal_category.left_unitor_conjugationView on Github →
2020-07-28 23:25
src/category_theory/monoidal/category.lean
feat(category_theory/monoidal): λ_ (𝟙_ C) = ρ_ (𝟙_ C) (#3556) …
Added category_theory.monoidal_category.left_unitor_conjugationView on Github →