mathlib3 documentation

data.polynomial.derivative

The derivative map on polynomials #

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

Main definitions #

noncomputable def polynomial.derivative {R : Type u} [semiring R] :

derivative p is the formal derivative of the polynomial p

Equations
theorem polynomial.derivative_apply {R : Type u} [semiring R] (p : polynomial R) :
polynomial.derivative p = p.sum (λ (n : ) (a : R), polynomial.C (a * n) * polynomial.X ^ (n - 1))
theorem polynomial.coeff_derivative {R : Type u} [semiring R] (p : polynomial R) (n : ) :
@[simp]
theorem polynomial.derivative_sum {R : Type u} {ι : Type y} [semiring R] {s : finset ι} {f : ι polynomial R} :
polynomial.derivative (s.sum (λ (b : ι), f b)) = s.sum (λ (b : ι), polynomial.derivative (f b))
@[simp]
theorem polynomial.iterate_derivative_C {R : Type u} {a : R} [semiring R] {k : } (h : 0 < k) :
@[simp]
theorem polynomial.iterate_derivative_one {R : Type u} [semiring R] {k : } (h : 0 < k) :
theorem polynomial.derivative_eval {R : Type u} [semiring R] (p : polynomial R) (x : R) :
polynomial.eval x (polynomial.derivative p) = p.sum (λ (n : ) (a : R), a * n * x ^ (n - 1))
theorem polynomial.coeff_iterate_derivative_as_prod_Ico {R : Type u} [semiring R] {k : } (p : polynomial R) (m : ) :
(polynomial.derivative^[k] p).coeff m = (finset.Ico m.succ (m + k.succ)).prod (λ (i : ), i) p.coeff (m + k)
theorem polynomial.coeff_iterate_derivative_as_prod_range {R : Type u} [semiring R] {k : } (p : polynomial R) (m : ) :
(polynomial.derivative^[k] p).coeff m = (finset.range k).prod (λ (i : ), m + k - i) p.coeff (m + k)
theorem polynomial.dvd_iterate_derivative_pow {R : Type u} [comm_semiring R] (f : polynomial R) (n : ) {m : } (c : R) (hm : m 0) :