feat(data/dfinsupp): copy map_range defs from finsupp (#7293)
This adds the bundled homs:
* `dfinsupp.map_range.add_monoid_hom`
* `dfinsupp.map_range.add_equiv`
* `dfinsupp.map_range.linear_map`
* `dfinsupp.map_range.linear_equiv`
and lemmas
* `dfinsupp.map_range_zero`
* `dfinsupp.map_range_add`
* `dfinsupp.map_range_smul`
For which we already have identical lemmas for `finsupp`.
Split from #7217, since `map_range.add_equiv` can be used in conjunction with `submonoid.mrange_restrict`
