Def adjoinOneAdj

Modification history

2024-05-16 11:37

Mathlib/Algebra/Category/MonCat/Adjunctions.lean

chore: namespace and tidy MonCat/GroupCat adjunctions (#12948)

Deleted adjoinOneAdj View on Github →

2023-07-01 16:46

Mathlib/Algebra/Category/MonCat/Adjunctions.lean

feat: port Algebra.Category.Mon.Adjunctions (#5648)

Added adjoinOneAdj View on Github →