mv_power_series

Stream: maths

[Yury G. Kudryashov]

@Johan Commelin Can we express exp(x + y) = exp x * exp y with the current state of mv_power_series? I mean, if I define def power_series.exp [field α] : power_series α := power_series.mk (λ n, 1 / n.fact)?

[Yury G. Kudryashov]

I guess, this should depend on something like comp (p : mv_power_series α) (q : mv_polynomial α) (h : C q = 0).

[Johan Commelin]

I don't think we have composition of formal power series atm

[Johan Commelin]

So it will require some work