Def MonCat.adjoinOneAdj

Modification history

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