Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-07-15 12:02 ecef6862

View on Github →

feat(algebra/category/Group): The forgetful-units adjunction between Group and Mon. (#15330)

Estimated changes

Modified src/algebra/category/Group/adjunctions.lean

added def CommGroup.forget₂_CommMon_adj

added def CommMon.units

added def Group.forget₂_Mon_adj

added def Mon.units