Def yonedaGrp

Modification history

2025-10-16 01:23

Mathlib/CategoryTheory/Monoidal/Cartesian/Grp_.lean

chore: rename `Grp_` to `Grp` (#30496) …

Modified yonedaGrp View on Github →

2025-10-12 18:01

Mathlib/CategoryTheory/Monoidal/Cartesian/Grp_.lean

chore: rename `Grp` to `GrpCat` (#30191) …

Modified yonedaGrp View on Github →

2025-05-11 10:35

Mathlib/CategoryTheory/Monoidal/Cartesian/Grp_.lean

feat: Yoneda for (comm) group objects (#24118) …

Added yonedaGrp View on Github →