Def GroupCat.abelianizeAdj

Modification history

2024-06-20 02:11
Mathlib/Algebra/Category/Grp/Adjunctions.lean
chore: Rename to `Grp` (#3731) …
Deleted GroupCat.abelianizeAdjView on Github →
2024-05-16 11:37
Mathlib/Algebra/Category/GroupCat/Adjunctions.lean
chore: namespace and tidy MonCat/GroupCat adjunctions (#12948)
Added GroupCat.abelianizeAdjView on Github →