Commit 2020-07-18 11:26 21a16834

View on Github →

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.

Estimated changes

Modified src/data/finsupp.lean

added theorem finsupp.on_finset_sum