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