Def CategoryTheory.LaxMonoidalFunctor.mapMonFunctor

Modification history

2023-06-07 05:59

Mathlib/CategoryTheory/Monoidal/Mon_.lean

feat: port CategoryTheory.Monoidal.Mon_ (#4763)

Added CategoryTheory.LaxMonoidalFunctor.mapMonFunctor View on Github →