Commit 2025-09-13 17:38 0f1f2179

View on Github →

chore: rename Mon_Class to MonObj (#28406) and Comon_Class to ComonObj. Grp_Class, CommGrp_Class and Mod_Class will follow. Zulip

Estimated changes

modified theorem Bimon_.compatibility
modified def Bimon_.mk'
modified def Bimon_.mk'X
modified theorem Bimon_.mul_counit
modified theorem Bimon_.one_comul
modified theorem comul_eq_lift
modified theorem counit_eq_toUnit
added theorem MonObj.comp_mul
added theorem MonObj.comp_one
added theorem MonObj.comp_pow
added theorem MonObj.lift_lift_assoc
added theorem MonObj.mul_comp
added theorem MonObj.mul_eq_mul
added theorem MonObj.one_comp
added theorem MonObj.one_eq_one
added theorem MonObj.pow_comp
deleted theorem Mon_Class.comp_mul
deleted theorem Mon_Class.comp_one
deleted theorem Mon_Class.comp_pow
deleted theorem Mon_Class.lift_lift_assoc
deleted theorem Mon_Class.mul_comp
deleted theorem Mon_Class.mul_eq_mul
deleted theorem Mon_Class.one_comp
deleted theorem Mon_Class.one_eq_one
deleted theorem Mon_Class.pow_comp
modified def CommMon_.mkIso'
modified theorem Comon_.tensorObj_comul'
modified theorem Comon_.tensorObj_comul
modified theorem Comon_.tensorObj_counit
modified theorem Grp_Class.ext
modified def Mod_.comap
modified structure Mod_
modified theorem Mod_Class.smul_eq_mul
added theorem MonObj.ext
added theorem MonObj.mul_assoc_flip
added theorem MonObj.mul_one_hom
added def MonObj.ofIso
added theorem MonObj.one_mul_hom
modified def Mon_.mkIso'
deleted theorem Mon_Class.ext
deleted theorem Mon_Class.mul_assoc_flip
deleted theorem Mon_Class.mul_one_hom
deleted def Mon_Class.ofIso
deleted theorem Mon_Class.one_mul_hom
added def MonObj.mopEquiv
deleted def Mon_Class.mopEquiv