Theorem Mon_.forgetMonoidal_ε

Modification history

2024-11-10 22:57
Mathlib/CategoryTheory/Monoidal/Mon_.lean
refactor(CategoryTheory/Monoidal): typeclasses Functor.LaxMonoidal, Functor.OplaxMonoidal and Functor.Monoidal (#17904) …
Deleted Mon_.forgetMonoidal_εView on Github →
2024-05-21 23:04
Mathlib/CategoryTheory/Monoidal/Mon_.lean
feat: the forgetful functor from `Mon_ C` to `C` is monoidal when `C` is braided (#12857)
Added Mon_.forgetMonoidal_εView on Github →