Commit 2023-03-14 15:28 15bde783

View on Github →

feat: port Data.Polynomial.Taylor (#2850)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Data/Polynomial/Taylor.lean

added theorem Polynomial.eq_zero_of_hasseDeriv_eq_zero

added theorem Polynomial.natDegree_taylor

added theorem Polynomial.sum_taylor_eq

added def Polynomial.taylor

added def Polynomial.taylorAlgHom

added theorem Polynomial.taylor_C

added theorem Polynomial.taylor_X

added theorem Polynomial.taylor_apply

added theorem Polynomial.taylor_coeff

added theorem Polynomial.taylor_coeff_one

added theorem Polynomial.taylor_coeff_zero

added theorem Polynomial.taylor_eval

added theorem Polynomial.taylor_eval_sub

added theorem Polynomial.taylor_injective

added theorem Polynomial.taylor_monomial

added theorem Polynomial.taylor_mul

added theorem Polynomial.taylor_one

added theorem Polynomial.taylor_taylor

added theorem Polynomial.taylor_zero'

added theorem Polynomial.taylor_zero