Theorem Finsupp.sum_cons'

Modification history

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