Commit 2024-05-16 11:37 b8d7525d

View on Github →

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

Estimated changes

Modified Mathlib/Algebra/Category/GroupCat/Adjunctions.lean

added def GroupCat.abelianize

added def GroupCat.abelianizeAdj

deleted def abelianize

deleted def abelianizeAdj

Modified Mathlib/Algebra/Category/MonCat/Adjunctions.lean

added def MonCat.adj

added def MonCat.adjoinOne

added def MonCat.adjoinOneAdj

added def MonCat.free

deleted def adj

deleted def adjoinOne

deleted def adjoinOneAdj

deleted def free