Commit 2023-10-17 17:20 b940be20

View on Github →

chore(Algebra/BigOperators/Finsupp): sums of Finsupp.single (#7716) This adds a new lemma to match the existing Pi lemma, and renames the existing lemmas to avoid inconsistent naming. The equivFunOnFinite lemma is motivated by #6657.

Estimated changes