feat(data/finsupp/pointwise): add a definition of the pointwise action of functions on finsupps (#10933)
feat(data/finsupp/pointwise): add a definition of the pointwise action of functions on finsupps (#10933)

I couldn't find this, and it seems like quite a natural way to talk about multiplying functions with finsupps.
I'm not sure what additional lemmas would be useful yet, as I don't have a particular application in mind at present so suggestions/additions are welcome





leanprover-community/mathlib,leanprover-community/mathlib