mathlib

4bf48590 - 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