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
fin n? Or should I create a
s : finset (A) and use
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):
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
Last updated: Aug 03 2023 at 10:10 UTC