mathlib

d3a46a7f - feat(algebra/big_operators): telescopic sums (#7470)

feat(algebra/big_operators): telescopic sums (#7470) This is restating things we already have in a form which is slightly more convenient for the liquid tensor experiment