Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-04-21 09:38 7db1181e

View on Github →

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

Estimated changes

added theorem dfinsupp.coe_zero
added theorem dfinsupp.map_range_add
added theorem dfinsupp.map_range_id
modified theorem dfinsupp.zero_apply