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

Modified src/algebra/group/hom.lean

deleted theorem add_monoid_hom.coe_of_map_sub

deleted theorem add_monoid_hom.map_sub

deleted def add_monoid_hom.of_map_sub

added theorem monoid_hom.coe_of_map_div

added theorem monoid_hom.map_div

added def monoid_hom.of_map_div

Modified src/algebra/group/hom_instances.lean

added theorem monoid_hom.map_div₂

added theorem monoid_hom.map_inv₂

added theorem monoid_hom.map_mul₂

added theorem monoid_hom.map_one₂