Sum over range

Stream: new members

[Violeta Hernández]

What's the preferred Mathlib form for summing a sequence over 0, 1, ..., n - 1? Is it ∑ k : Fin n, _, ∑ k ∈ range n, _, or something else?

[Kevin Buzzard]

Does _ want to eat a natural, an integer, a rational, a term of type Fin n,...?

[Violeta Hernández]

Something in an arbitrary field

[Violeta Hernández]

I figured that since I wanted to use docs#geom_sum_eq I'd be better off using the second form

[Kevin Buzzard]

It's also far more fiddly to do induction with the first form

[Zhang Qinchuan]

Personally, I prefer Finset.range since Nat is easier to handle compared to Fin n.