Is there (mv) power series version for expand_char

Stream: Is there code for X?

[Wenrong Zou]

Is there a (mv) power series version of Polynomial.expand_char or has anyone already done this? (I don't find MvPolynomial.expand_char in mathlib, it can be easily proved by current API). If not, I was wondering whether I could claim I will work on this since I would need it in my project. Also I am not sure whether it is useful to build the function expand for (mv) power series (not sure someone has already done this). If it is useful to define it, I could also do it. Thanks in advance!

[Johan Commelin]

Probably it's missing. In general the API for polynomials is much more complete than the one for power series.

If you decide to contribute it, feel free to ping me for review on your PR. And it would be great if you could follow the Polynomial API as inspiration.

[Wenrong Zou]

Thank you for your comment. I would try to do it and PR it in the next few days. I would follow the style in Polynomial. Thanks!

[Yaël Dillies]

Note to future self: Unify all of these

[Wenrong Zou]

Thank you for your advice! But currently, my idea to do this for (mv) power series is to do truncation first and use the result for (mv) polynomial, since we cannot do induction for (mv) power series. I am not sure whether there is a better way to do this. So somehow we need to the result for polynomial to prove the result for power series.