Formal Series

Stream: Is there code for X?

[THEODORE GONZALES]

Is there code for formal series with coefficients in some type? Ideally this would be something that, in context A: Type, and f: Z -> A then be able to check if f has finite support if zero objects make sense in A .

[Anne Baanen]

Sequences with finite support are called docs#finsupp so e.g. ℤ →₀ A is the type of all integer-indexed sequences with only finitely many nonzero values.

[Anne Baanen]

For series maybe you want more something like docs#power_series?

[Junyan Xu]

we also have docs#function.support and docs#set.finite, and you can construct a finsupp that way: docs#finsupp.of_support_finite

[THEODORE GONZALES]

Thank you !