## Stream: general

### Topic: finite sums

#### Koundinya Vajjha (Jun 11 2019 at 14:45):

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 (Jun 11 2019 at 14:46):

The library for the latter option is quite extensive

#### Chris Hughes (Jun 11 2019 at 14:47):

I think tsum is just for infinite sums.

#### Koundinya Vajjha (Jun 11 2019 at 14:47):

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

Last updated: May 14 2021 at 12:18 UTC