Zulip Chat Archive

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: Dec 20 2023 at 11:08 UTC