Commit 2022-01-10 23:30 4bf48590
View on Github →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