mathlib3

52a2e8b9 - chore(algebra/group/hom_instances): add monoid_hom versions of linear_map lemmas (#8461)

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.