Difference between ∑ᶠ and ∑'

Stream: mathlib4

[Colin Jones ⚛️]

What is the pragmatic difference between ∑ᶠ from Mathlib.Algebra.BigOperators.Finprod and ∑' from Mathlib.Topology.Algebra.InfiniteSum.Basic ?

[Patrick Massot]

You mean docs#finsum and docs#tsum, right?

[Patrick Massot]

The first one is pure algebra, it returns something non-zero only if the support of the summed function is finite. The second one incorporate topology and can return something non-zero even for function with infinite support.

[Patrick Massot]

See https://en.wikipedia.org/wiki/Convergent_series.

[Colin Jones ⚛️]

Yes, those ones. Okay that makes sense, thank you