mathlib3

4ddae3db - feat(ring_theory/power_series): define power series for `exp`, `sin`, `cos`, and `1 / (u - x)`. (#5432)

feat(ring_theory/power_series): define power series for `exp`, `sin`, `cos`, and `1 / (u - x)`. (#5432) This PR defines `power_series.exp` etc to be formal power series for the corresponding functions. Once we have a bridge to `is_analytic`, we should redefine `complex.exp` etc using these power series.