Mathlib Changelog
v4
Changelog
About
Github
Theorem
Comon_.forget_η
Modification history
2025-06-04 18:15
Mathlib/CategoryTheory/Monoidal/Comon_.lean
feat(CategoryTheory/Monoidal): define Mon_ by using Mon_Class (#24646) …
Modified
Comon_.forget_η
View on Github →
2024-11-10 22:57
Mathlib/CategoryTheory/Monoidal/Comon_.lean
refactor(CategoryTheory/Monoidal): typeclasses Functor.LaxMonoidal, Functor.OplaxMonoidal and Functor.Monoidal (#17904) …
Added
Comon_.forget_η
View on Github →