Commit 2026-03-27 18:43 e4f069ee

View on Github →

feat(CategoryTheory/Monoidal): use to_additive for the Yoneda embedding of monoid objects (#37265)

Estimated changes

Modified Mathlib/CategoryTheory/Monoidal/Cartesian/Mon_.lean

modified theorem CategoryTheory.Mon.Hom.hom_mul

modified theorem CategoryTheory.Mon.Hom.hom_one

modified theorem CategoryTheory.Mon.Hom.hom_pow

modified theorem CategoryTheory.Mon.fst_hom

modified theorem CategoryTheory.Mon.hom_mul

modified theorem CategoryTheory.Mon.hom_one

modified theorem CategoryTheory.Mon.lift_hom

modified theorem CategoryTheory.Mon.snd_hom