Group): The forgetful-units adjunction between `Group` and `Mon`. (#15330)

Commit

3 years ago

feat(algebra/category/Group): The forgetful-units adjunction between `Group` and `Mon`. (#15330) Co-authored-by: Andrew Yang <36414270+erdOne@users.noreply.github.com>

Author

erdOne

Parents

863a30af

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

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