Theorem Finsupp.sum_cons

Modification history

2025-03-10 16:50
Mathlib/Algebra/BigOperators/Finsupp/Basic.lean
chore(Algebra/BigOperators): reverse `Finsupp` <-> `Fin` import direction (#22770) …
Modified Finsupp.sum_consView on Github →
2023-09-08 04:16
Mathlib/Algebra/BigOperators/Finsupp.lean
feat: add Finsupp.sum_cons (#6604) …
Added Finsupp.sum_consView on Github →