finsupp.map_range

Stream: Is there code for X?

[Heather Macbeth]

The dfinsupp version of map_range is more flexible than the finsupp version, in that it allows for homomorphisms varying by index:
docs#finsupp.map_range
docs#dfinsupp.map_range
Is there a fast way to get this flexibility in the finsupp case?

import linear_algebra.finsupp

noncomputable theory
variables {ι : Type*} {R : Type*} [ring R]
variables {M : Type*} [add_comm_group M] [module R M]
variables {N : Type*} [add_comm_group N] [module R N]

example (f : ι → (M →ₗ[R] N)) : (ι →₀ M) →ₗ[R] (ι →₀ N) := sorry

[Eric Wieser]

Presumably the thing to do is just to modify finsupp.map_range