Zulip Chat Archive

Stream: general

Topic: finite sums


view this post on Zulip 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?

view this post on Zulip Johan Commelin (Jun 11 2019 at 14:46):

The library for the latter option is quite extensive

view this post on Zulip Chris Hughes (Jun 11 2019 at 14:47):

I think tsum is just for infinite sums.

view this post on Zulip 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