Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-04-14 03:47 500301e7

View on Github →

feat(algebra/group/hom): monoid_with_zero_hom.to_monoid_hom_injective and co. (#7174) This came up in #6788.

Estimated changes