Commit 2026-04-09 16:23 eca733c7

View on Github →

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

Estimated changes

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

modified theorem CategoryTheory.Functor.map_inv'

modified theorem CategoryTheory.Grp.Hom.hom_hom_div

modified theorem CategoryTheory.Grp.Hom.hom_hom_inv

modified theorem CategoryTheory.Grp.Hom.hom_hom_zpow

modified theorem CategoryTheory.Grp.Hom.hom_mul

modified theorem CategoryTheory.Grp.Hom.hom_one

modified theorem CategoryTheory.Grp.Hom.hom_pow

modified theorem CategoryTheory.Grp.hom_mul

modified theorem CategoryTheory.Grp.hom_one