mathlib documentation

data.polynomial.taylor

Taylor expansions of polynomials #

Main declarations #

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

The Taylor expansion of a polynomial f at r.

Equations
theorem polynomial.taylor_apply {R : Type u_1} [semiring R] (r : R) (f : polynomial R) :
@[simp]
theorem polynomial.taylor_C {R : Type u_1} [semiring R] (r x : R) :
@[simp]
theorem polynomial.taylor_one {R : Type u_1} [semiring R] (r : R) :
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]
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