## Stream: maths

### Topic: mv_power_series

#### Yury G. Kudryashov (Sep 24 2020 at 22:59):

@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 (Sep 24 2020 at 23:02):

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

#### Johan Commelin (Sep 25 2020 at 03:54):

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

#### Johan Commelin (Sep 25 2020 at 03:54):

So it will require some work

Last updated: May 18 2021 at 08:14 UTC