Commit 2025-11-08 15:24 7a8ea2bb

View on Github →

feat: commutative monoids are internal monoids (#29765) From Toric

Estimated changes

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

added theorem CategoryTheory.Grp.Hom.hom_div

added theorem CategoryTheory.Grp.Hom.hom_inv

added theorem CategoryTheory.Grp.Hom.hom_mul

added theorem CategoryTheory.Grp.Hom.hom_one

added theorem CategoryTheory.Grp.Hom.hom_pow

added theorem CategoryTheory.Grp.Hom.hom_zpow

added theorem CategoryTheory.Grp.hom_mul

added theorem CategoryTheory.Grp.hom_one

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

added theorem CategoryTheory.Mon.Hom.hom_mul

added theorem CategoryTheory.Mon.Hom.hom_one

added theorem CategoryTheory.Mon.Hom.hom_pow

added theorem CategoryTheory.Mon.hom_mul

added theorem CategoryTheory.Mon.hom_one

Modified Mathlib/CategoryTheory/Monoidal/Grp_.lean

deleted def CategoryTheory.Grp.toMon