mathlib

98643bca - feat(algebra/big_operators/intervals): summation by parts (#11814)

feat(algebra/big_operators/intervals): summation by parts (#11814) Add the "summation by parts" identity over intervals of natural numbers, as well as some helper lemmas.