Question about sum_range_succ

Stream: general

[Mattia Bottoni]

Hi everybody :)

I wanted to use sum_range_succ in a proof, but I am very confused about this theorem.

sum_range_succ.png

I found this in the Lean 4 documentation side. Why do they add f n at the end and not f (n+1). The last "element" of the sum is (n+1) and not n.

What am I missing?

Thanks in advance!
Matt

[Eric Wieser]

docs#Finset.range does not include the upper bound

[Kevin Buzzard]

It also starts at 0 not 1, so there are $n$ numbers in range n.

[Mattia Bottoni]

Ah I see!
Thank you both very much :)