Def CategoryTheory.yonedaCommGrpGrpObj

Modification history

2025-11-09 12:23
Mathlib/CategoryTheory/Monoidal/Cartesian/CommGrp_.lean
feat: yoneda embedding of `CommGrp C` into presheaves of groups (#31390) …
Added CategoryTheory.yonedaCommGrpGrpObjView on Github →