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