Commit 2025-07-12 14:42 db7a73c5

View on Github →

feat: CommGrp-valued Yoneda embedding (#24778) From Toric

Estimated changes

Modified Mathlib.lean

Created Mathlib/Algebra/Category/Grp/Yoneda.lean

added def CommGrp.coyoneda

added def CommGrp.coyonedaForget

added def CommGrp.coyonedaType

Created Mathlib/Algebra/Category/MonCat/Yoneda.lean

added def CommMonCat.coyoneda

added def CommMonCat.coyonedaForget

added def CommMonCat.coyonedaType

Modified Mathlib/CategoryTheory/Preadditive/Yoneda/Basic.lean

added def AddCommGrp.preadditiveCoyonedaIso