mathlib3 documentation

data.polynomial.taylor

Taylor expansions of polynomials #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

Main declarations #

noncomputable def polynomial.taylor {R : Type u_1} [semiring R] (r : R) :

The Taylor expansion of a polynomial f at r.

Equations
@[simp]
theorem polynomial.taylor_zero {R : Type u_1} [semiring R] (f : polynomial R) :
@[simp]
theorem polynomial.taylor_one {R : Type u_1} [semiring R] (r : R) :
@[simp]
theorem polynomial.taylor_coeff {R : Type u_1} [semiring R] (r : R) (f : polynomial R) (n : ) :

The kth coefficient of polynomial.taylor r f is (polynomial.hasse_deriv k f).eval r.

@[simp]
theorem polynomial.taylor_coeff_zero {R : Type u_1} [semiring R] (r : R) (f : polynomial R) :
@[simp]
@[simp]
theorem polynomial.taylor_mul {R : Type u_1} [comm_semiring R] (r : R) (p q : polynomial R) :
noncomputable def polynomial.taylor_alg_hom {R : Type u_1} [comm_semiring R] (r : R) :

polynomial.taylor as a alg_hom for commutative semirings

Equations
@[simp]
theorem polynomial.taylor_eval {R : Type u_1} [comm_semiring R] (r : R) (f : polynomial R) (s : R) :
theorem polynomial.taylor_eval_sub {R : Type u_1} [comm_ring R] (r : R) (f : polynomial R) (s : R) :
theorem polynomial.eq_zero_of_hasse_deriv_eq_zero {R : Type u_1} [comm_ring R] (f : polynomial R) (r : R) (h : (k : ), polynomial.eval r ((polynomial.hasse_deriv k) f) = 0) :
f = 0
theorem polynomial.sum_taylor_eq {R : Type u_1} [comm_ring R] (f : polynomial R) (r : R) :

Taylor's formula.