Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-12-22 07:50 4ddae3db

View on Github →

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.

Estimated changes

modified theorem ring_hom.map_eq_zero
added theorem units.coe_map_inv
modified theorem is_R_or_C.conj_eq_zero
added theorem power_series.coeff_exp
added def power_series.cos
added def power_series.exp
added theorem power_series.map_cos
added theorem power_series.map_exp
added theorem power_series.map_sin
added def power_series.sin