Commit 2025-06-17 16:39 d3e49aad

View on Github →

feat: X ⟶ M is a commutative monoid if M is a commutative monoid object (#24769) Also add a shortcut Grp_.homMk of Mon_.Hom.mk for Grp_, provide Yoneda-like lemmas for monoid morphisms and bundle Mon_.ext into an Injective lemma. Unsimp Grp_Class.tensorHom_inv_inv_mul since it loops with IsMon_Hom.mul_hom + IsMon_Hom ι. From Toric

Estimated changes

added def Grp_.homMk
added theorem Grp_Class.comp_div
added theorem Grp_Class.comp_zpow
added theorem Grp_Class.div_comp
added theorem Grp_Class.zpow_comp
added theorem Mon_Class.comp_pow
added theorem Mon_Class.pow_comp
added theorem Grp_Class.mul_inv_rev
modified theorem Mon_.Hom.ext'
added theorem Mon_.hom_injective