Commit 2023-06-28 16:07 e95d03d4

View on Github →

feat: port CategoryTheory.Monad.EquivMon (#5086)

Estimated changes

Modified Mathlib.lean

Modified Mathlib/CategoryTheory/Monad/Basic.lean

Created Mathlib/CategoryTheory/Monad/EquivMon.lean

added def CategoryTheory.Monad.monToMonad

added def CategoryTheory.Monad.monadMonEquiv

added def CategoryTheory.Monad.monadToMon

added def CategoryTheory.Monad.ofMon

added theorem CategoryTheory.Monad.ofMon_obj

added def CategoryTheory.Monad.toMon

Modified Mathlib/CategoryTheory/Monoidal/End.lean

added theorem CategoryTheory.endofunctorMonoidalCategory_associator_hom_app

added theorem CategoryTheory.endofunctorMonoidalCategory_associator_inv_app

added theorem CategoryTheory.endofunctorMonoidalCategory_leftUnitor_hom_app

added theorem CategoryTheory.endofunctorMonoidalCategory_leftUnitor_inv_app

added theorem CategoryTheory.endofunctorMonoidalCategory_rightUnitor_hom_app

added theorem CategoryTheory.endofunctorMonoidalCategory_rightUnitor_inv_app

added theorem CategoryTheory.endofunctorMonoidalCategory_tensorMap_app

added theorem CategoryTheory.endofunctorMonoidalCategory_tensorObj_map

added theorem CategoryTheory.endofunctorMonoidalCategory_tensorObj_obj

added theorem CategoryTheory.endofunctorMonoidalCategory_tensorUnit_map

added theorem CategoryTheory.endofunctorMonoidalCategory_tensorUnit_obj

Modified Mathlib/CategoryTheory/Shift/Basic.lean