finite sums

Stream: general

[Koundinya Vajjha]

Sorry for bringing this up again, but what is the mathlib recommended way to talk about finite sums?
Is it a tsum over fin n? Or should I create a s : finset (A) and use s.sum?

[Johan Commelin]

The library for the latter option is quite extensive

[Chris Hughes]

I think tsum is just for infinite sums.

[Koundinya Vajjha]

Thank you! So I will use s : finset (fin n) and s.sum