Commit 2025-05-11 10:35 c9466b7e

View on Github →

feat: Yoneda for (comm) group objects (#24118) And make the API between monoid and group objects more alike. From Toric

Estimated changes

added theorem Grp_Class.comp_inv
added theorem Grp_Class.inv_comp
added theorem Grp_Class.inv_eq_inv
added theorem Hom.inv_def
added theorem essImage_yonedaGrp
added def yonedaGrp
added def yonedaGrpObj
added theorem yonedaGrp_naturality
added theorem Hom.mul_def
added theorem Hom.one_def
added theorem Mon_Class.comp_mul
added theorem Mon_Class.comp_one
added theorem Mon_Class.mul_comp
added theorem Mon_Class.mul_eq_mul
added theorem Mon_Class.one_comp
added theorem Mon_Class.one_eq_one
added theorem essImage_yonedaMon
added def yonedaMon
added def yonedaMonObj
added theorem yonedaMon_naturality
deleted theorem essImage_yonedaMon
deleted def monoidOfMon_Class
deleted def yonedaMon
deleted def yonedaMonObj
deleted theorem yonedaMon_naturality