Def Grp_.mk'

Modification history

2025-06-15 16:47
Mathlib/CategoryTheory/Monoidal/Grp_.lean
chore: deprecate `Grp_.mk'` (#25896) …
Deleted Grp_.mk'View on Github →
2025-03-05 17:48
Mathlib/CategoryTheory/Monoidal/Grp_.lean
feat(CategoryTheory): API for group objects (#22168)
Added Grp_.mk'View on Github →