Commit 2021-04-02 09:16 394719f5

chore(data/finsupp): lemmas about map_range and map_domain (#6976) This proves some functorial properties:

• finsupp.map_range_id
• finsupp.map_range_comp Adds the new definitions to match finsupp.map_range.add_monoid_hom, and uses them to golf some proofs:
• finsupp.map_range.zero_hom, which is map_domain as a zero_hom
• finsupp.map_range.add_equiv, which is map_range as an add_equiv
• finsupp.map_range.linear_map, which is map_range as a linear_map
• finsupp.map_range.linear_equiv, which is map_range as a linear_equiv
• finsupp.map_domain.add_monoid_hom, which is map_domain as an add_monoid_hom Shows the functorial properties of these bundled definitions:
• finsupp.map_range.zero_hom_id, finsupp.map_range.zero_hom_comp
• finsupp.map_range.add_monoid_hom_id, finsupp.map_range.add_monoid_hom_comp
• finsupp.map_range.add_equiv_refl, finsupp.map_range.add_equiv_trans
• finsupp.map_range.linear_map_id, finsupp.map_range.linear_map_comp
• finsupp.map_range.linear_equiv_refl, finsupp.map_range.linear_equiv_trans
• finsupp.map_domain.add_monoid_hom_id, finsupp.map_domain.add_monoid_hom_comp And shows that map_range and map_domain commute when the range-map preserves addition:
• finsupp.map_domain_map_range