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.