Commit 2025-09-14 15:36 5fc66a8f

View on Github →

chore: rename Mod_Class to ModObj (#29641) and similarly for Hopf_Class and IsCommMon. This is a follow-up to #28406.

Estimated changes

modified def CommGrp_.mkIso'
modified def CommMon_.mkIso'
added theorem HopfObj.antipode_comul
added theorem HopfObj.hom_antipode
added theorem HopfObj.mul_antipode
added theorem HopfObj.one_antipode
deleted theorem Hopf_Class.antipode_comul
deleted theorem Hopf_Class.hom_antipode
deleted theorem Hopf_Class.mul_antipode
deleted theorem Hopf_Class.one_antipode
added theorem ModObj.assoc_flip
added theorem ModObj.ext
added theorem ModObj.mul_smul
added theorem ModObj.one_smul
added theorem ModObj.smul_eq_mul
modified def Mod_.Hom.mk''
deleted theorem Mod_Class.assoc_flip
deleted theorem Mod_Class.ext
deleted theorem Mod_Class.mul_smul
deleted theorem Mod_Class.one_smul
deleted theorem Mod_Class.smul_eq_mul