# mathlib3documentation

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 #

• polynomial.taylor: the Taylor expansion of the polynomial f at r
• polynomial.taylor_coeff: the kth coefficient of taylor r f is (polynomial.hasse_deriv k f).eval r
• polynomial.eq_zero_of_hasse_deriv_eq_zero: the identity principle: a polynomial is 0 iff all its Hasse derivatives are zero
noncomputable 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) :
f = f.comp
@[simp]
theorem polynomial.taylor_X {R : Type u_1} [semiring R] (r : R) :
@[simp]
theorem polynomial.taylor_C {R : Type u_1} [semiring R] (r x : R) :
@[simp]
theorem polynomial.taylor_zero' {R : Type u_1} [semiring R] :
theorem polynomial.taylor_zero {R : Type u_1} [semiring R] (f : polynomial R) :
f = f
@[simp]
theorem polynomial.taylor_one {R : Type u_1} [semiring R] (r : R) :
1 =
@[simp]
theorem polynomial.taylor_monomial {R : Type u_1} [semiring R] (r : R) (i : ) (k : R) :
( k) = * ^ i
theorem polynomial.taylor_coeff {R : Type u_1} [semiring R] (r : R) (f : polynomial R) (n : ) :
( f).coeff n = f)

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) :
( f).coeff 0 =
@[simp]
theorem polynomial.taylor_coeff_one {R : Type u_1} [semiring R] (r : R) (f : polynomial R) :
( f).coeff 1 =
@[simp]
theorem polynomial.nat_degree_taylor {R : Type u_1} [semiring R] (p : polynomial R) (r : R) :
@[simp]
theorem polynomial.taylor_mul {R : Type u_1} (r : R) (p q : polynomial R) :
(p * q) = p * q
noncomputable def polynomial.taylor_alg_hom {R : Type u_1} (r : R) :

polynomial.taylor as a alg_hom for commutative semirings

Equations
@[simp]
theorem polynomial.taylor_alg_hom_apply {R : Type u_1} (r : R) (ᾰ : polynomial R) :
=
theorem polynomial.taylor_taylor {R : Type u_1} (f : polynomial R) (r s : R) :
( f) = (polynomial.taylor (r + s)) f
theorem polynomial.taylor_eval {R : Type u_1} (r : R) (f : polynomial R) (s : R) :
( f) = polynomial.eval (s + r) f
theorem polynomial.taylor_eval_sub {R : Type u_1} [comm_ring R] (r : R) (f : polynomial R) (s : R) :
polynomial.eval (s - r) ( f) =
theorem polynomial.taylor_injective {R : Type u_1} [comm_ring R] (r : R) :
theorem polynomial.eq_zero_of_hasse_deriv_eq_zero {R : Type u_1} [comm_ring R] (f : polynomial R) (r : R) (h : (k : ), f) = 0) :
f = 0
theorem polynomial.sum_taylor_eq {R : Type u_1} [comm_ring R] (f : polynomial R) (r : R) :
( f).sum (λ (i : ) (a : R), * ^ i) = f

Taylor's formula.