Mathlib Changelog
v4
Changelog
About
Github
Commit
2025-11-09 12:23
8352e7bd
View on Github →
feat: yoneda embedding of
CommGrp C
into presheaves of groups (
#31390
) From Toric
Estimated changes
Modified
Mathlib/CategoryTheory/Monoidal/Cartesian/CommGrp_.lean
added
def
CategoryTheory.yonedaCommGrpGrp
added
def
CategoryTheory.yonedaCommGrpGrpObj
Modified
Mathlib/CategoryTheory/Monoidal/CommGrp_.lean
deleted
def
CategoryTheory.CommGrp.toGrp