Theorem CategoryTheory.endofunctorMonoidalCategory_leftUnitor_inv_app

Modification history

2023-06-28 16:07
Mathlib/CategoryTheory/Monoidal/End.lean
feat: port CategoryTheory.Monad.EquivMon (#5086)
Added CategoryTheory.endofunctorMonoidalCategory_leftUnitor_inv_appView on Github →