Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-02-10 21:01 6e52dfe3

View on Github →

feat(algebra/category/Group/adjunctions): adjunction of abelianization and forgetful functor (#6154) Abelianization has been defined in group_theory/abelianization without realising it in category theory. This PR adds this feature. Furthermore, a module doc for abelianization is added and the one for adjunctions is expanded.

Estimated changes