Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-08-01 21:03 52a2e8b9

View on Github →

chore(algebra/group/hom_instances): add monoid_hom versions of linear_map lemmas (#8461) I mainly want the additive versions, but we may as well get the multiplicative ones too. This also adds the missing monoid_hom.map_div and some other division versions of subtraction lemmas.

Estimated changes