Commit 2023-06-21 01:06 b5be6245

View on Github →

feat: port Algebra.Category.GroupCat.Adjunctions (#5292)

Estimated changes

Modified Mathlib.lean

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

added def AddCommGroupCat.adj

added def AddCommGroupCat.free

added theorem AddCommGroupCat.free_map_coe

added theorem AddCommGroupCat.free_obj_coe

added def CommGroupCat.forget₂CommMonAdj

added def CommMonCat.units

added def GroupCat.adj

added def GroupCat.forget₂MonAdj

added def GroupCat.free

added def MonCat.units

added def abelianize

added def abelianizeAdj