# mathlib3documentation

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 #

• polynomial.derivative: The formal derivative of polynomials, expressed as a linear map.
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) :
= 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 : ) :
= p.coeff (n + 1) * (n + 1)
@[simp]
theorem polynomial.derivative_zero {R : Type u} [semiring R] :
@[simp]
theorem polynomial.iterate_derivative_zero {R : Type u} [semiring R] {k : } :
@[simp]
theorem polynomial.derivative_monomial {R : Type u} [semiring R] (a : R) (n : ) :
theorem polynomial.derivative_C_mul_X {R : Type u} [semiring R] (a : R) :
theorem polynomial.derivative_C_mul_X_pow {R : Type u} [semiring R] (a : R) (n : ) :
theorem polynomial.derivative_C_mul_X_sq {R : Type u} [semiring R] (a : R) :
@[simp]
theorem polynomial.derivative_X_pow {R : Type u} [semiring R] (n : ) :
= * polynomial.X ^ (n - 1)
@[simp]
theorem polynomial.derivative_X_sq {R : Type u} [semiring R] :
@[simp]
theorem polynomial.derivative_C {R : Type u} [semiring R] {a : R} :
@[simp]
theorem polynomial.derivative_X {R : Type u} [semiring R] :
@[simp]
theorem polynomial.derivative_one {R : Type u} [semiring R] :
@[simp]
theorem polynomial.derivative_bit0 {R : Type u} [semiring R] {a : polynomial R} :
@[simp]
theorem polynomial.derivative_bit1 {R : Type u} [semiring R] {a : polynomial R} :
@[simp]
theorem polynomial.derivative_add {R : Type u} [semiring R] {f g : polynomial R} :
@[simp]
theorem polynomial.derivative_X_add_C {R : Type u} [semiring R] (c : R) :
@[simp]
theorem polynomial.iterate_derivative_add {R : Type u} [semiring R] {f g : polynomial R} {k : } :
@[simp]
theorem polynomial.derivative_sum {R : Type u} {ι : Type y} [semiring R] {s : finset ι} {f : ι } :
polynomial.derivative (s.sum (λ (b : ι), f b)) = s.sum (λ (b : ι), polynomial.derivative (f b))
@[simp]
theorem polynomial.derivative_smul {R : Type u} [semiring R] {S : Type u_1} [monoid S] [ R] [ R] (s : S) (p : polynomial R) :
@[simp]
theorem polynomial.iterate_derivative_smul {R : Type u} [semiring R] {S : Type u_1} [monoid S] [ R] [ R] (s : S) (p : polynomial R) (k : ) :
@[simp]
theorem polynomial.iterate_derivative_C_mul {R : Type u} [semiring R] (a : R) (p : polynomial R) (k : ) :
theorem polynomial.of_mem_support_derivative {R : Type u} [semiring R] {p : polynomial R} {n : } (h : n ) :
n + 1 p.support
theorem polynomial.degree_derivative_lt {R : Type u} [semiring R] {p : polynomial R} (hp : p 0) :
@[simp]
theorem polynomial.derivative_nat_cast {R : Type u} [semiring R] {n : } :
theorem polynomial.iterate_derivative_eq_zero {R : Type u} [semiring R] {p : polynomial R} {x : } (hx : p.nat_degree < x) :
@[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) :
@[simp]
theorem polynomial.iterate_derivative_X {R : Type u} [semiring R] {k : } (h : 1 < k) :
@[simp]
theorem polynomial.derivative_eval {R : Type u} [semiring R] (p : polynomial R) (x : R) :
= p.sum (λ (n : ) (a : R), a * n * x ^ (n - 1))
@[simp]
theorem polynomial.derivative_map {R : Type u} {S : Type v} [semiring R] [semiring S] (p : polynomial R) (f : R →+* S) :
@[simp]
theorem polynomial.iterate_derivative_map {R : Type u} {S : Type v} [semiring R] [semiring S] (p : polynomial R) (f : R →+* S) (k : ) :
theorem polynomial.derivative_nat_cast_mul {R : Type u} [semiring R] {n : } {f : polynomial R} :
theorem polynomial.mem_support_derivative {R : Type u} [semiring R] (p : polynomial R) (n : ) :
n + 1 p.support
@[simp]
theorem polynomial.degree_derivative_eq {R : Type u} [semiring R] (p : polynomial R) (hp : 0 < p.nat_degree) :
theorem polynomial.coeff_iterate_derivative_as_prod_Ico {R : Type u} [semiring R] {k : } (p : polynomial R) (m : ) :
= (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 : ) :
= (finset.range k).prod (λ (i : ), m + k - i) p.coeff (m + k)
theorem polynomial.derivative_pow_succ {R : Type u} (p : polynomial R) (n : ) :
theorem polynomial.derivative_pow {R : Type u} (p : polynomial R) (n : ) :
polynomial.derivative (p ^ n) = * p ^ (n - 1) *
theorem polynomial.dvd_iterate_derivative_pow {R : Type u} (f : polynomial R) (n : ) {m : } (c : R) (hm : m 0) :
theorem polynomial.derivative_X_add_C_pow {R : Type u} (c : R) (m : ) :
= * ^ (m - 1)
theorem polynomial.derivative_X_add_C_sq {R : Type u} (c : R) :
theorem polynomial.iterate_derivative_X_add_pow {R : Type u} (n k : ) (c : R) :
= ((finset.range k).prod (λ (i : ), n - i)) * ^ (n - k)
theorem polynomial.derivative_comp {R : Type u} (p q : polynomial R) :
theorem polynomial.derivative_eval₂_C {R : Type u} (p q : polynomial R) :

Chain rule for formal derivative of polynomials.

theorem polynomial.derivative_prod {R : Type u} {ι : Type y} {s : multiset ι} {f : ι } :
= (multiset.map (λ (i : ι), (s.erase i)).prod * polynomial.derivative (f i)) s).sum
@[simp]
theorem polynomial.derivative_neg {R : Type u} [ring R] (f : polynomial R) :
@[simp]
theorem polynomial.iterate_derivative_neg {R : Type u} [ring R] {f : polynomial R} {k : } :
@[simp]
theorem polynomial.derivative_sub {R : Type u} [ring R] {f g : polynomial R} :
@[simp]
theorem polynomial.derivative_X_sub_C {R : Type u} [ring R] (c : R) :
@[simp]
theorem polynomial.iterate_derivative_sub {R : Type u} [ring R] {k : } {f g : polynomial R} :
@[simp]
theorem polynomial.derivative_int_cast {R : Type u} [ring R] {n : } :
theorem polynomial.derivative_int_cast_mul {R : Type u} [ring R] {n : } {f : polynomial R} :
theorem polynomial.eval_multiset_prod_X_sub_C_derivative {R : Type u} [comm_ring R] {S : multiset R} {r : R} (hr : r S) :
(polynomial.derivative (multiset.map (λ (a : R), S).prod) = (multiset.map (λ (a : R), r - a) (S.erase r)).prod
theorem polynomial.derivative_X_sub_C_pow {R : Type u} [comm_ring R] (c : R) (m : ) :
= * ^ (m - 1)
theorem polynomial.derivative_X_sub_C_sq {R : Type u} [comm_ring R] (c : R) :
theorem polynomial.iterate_derivative_X_sub_pow {R : Type u} [comm_ring R] (n k : ) (c : R) :
= ((finset.range k).prod (λ (i : ), n - i)) * ^ (n - k)