mathlib3

21a16834 - feat(data/finsupp): sums over on_finset (#3427)

feat(data/finsupp): sums over on_finset (#3427) There aren't many lemmas about `finsupp.on_finset`. Add one that's useful for manipulating sums over `on_finset`.