sum grouping adjacent terms

Stream: maths

[Daniel Selsam]

Does mathlib have some variant of https://github.com/openai/miniF2F/blob/main/lean/src/test.lean#L1332-L1341?

[Ruben Van de Velde]

I don't think I've seen anything like that, but could be added pretty easily, I guess

[Daniel Selsam]

Ruben Van de Velde said:

I don't think I've seen anything like that, but could be added pretty easily, I guess

Thanks. Happy to PR it -- where would it go?

[Ruben Van de Velde]

Big operators/basic, probably? (On mobile, can't link)

[Eric Wieser]

Maybe generalize it to

∑ k in finset.range (m * n), f k = ∑ k in finset.range n, ∑ i in finset.range m, f (m * k + i)

so that we can group triples as well?

[Eric Wieser]

(and of course to_additiveize it)

[Eric Wieser]

I was hoping docs#finset.sum_partition could produce a slick proof, but we're missing a lot of the machinery