defs): add add_monoid_hom_class versions of map_range (#17738)

Commit

3 years ago

feat(data/finsupp/defs): add add_monoid_hom_class versions of map_range (#17738) - [x] depends on: #17717 Co-authored-by: Eric Wieser <wieser.eric@gmail.com>

Author

Multramate

Parents

43a289b5

mathlib 3c71503b - feat(data/finsupp/defs): add add_monoid_hom_class versions of map_range (#17738)

mathlib
3c71503b - feat(data/finsupp/defs): add add_monoid_hom_class versions of map_range (#17738)