# Documentation

Mathlib.Data.Polynomial.Derivative

# The derivative map on polynomials #

## Main definitions #

• Polynomial.derivative: The formal derivative of polynomials, expressed as a linear map.
def Polynomial.derivative {R : Type u} [] :

derivative p is the formal derivative of the polynomial p

Instances For
theorem Polynomial.derivative_apply {R : Type u} [] (p : ) :
Polynomial.derivative p = Polynomial.sum p fun n a => Polynomial.C (a * n) * Polynomial.X ^ (n - 1)
theorem Polynomial.coeff_derivative {R : Type u} [] (p : ) (n : ) :
Polynomial.coeff (Polynomial.derivative p) n = Polynomial.coeff p (n + 1) * (n + 1)
theorem Polynomial.derivative_zero {R : Type u} [] :
Polynomial.derivative 0 = 0
@[simp]
theorem Polynomial.iterate_derivative_zero {R : Type u} [] {k : } :
@[simp]
theorem Polynomial.derivative_monomial {R : Type u} [] (a : R) (n : ) :
Polynomial.derivative (↑() a) = ↑(Polynomial.monomial (n - 1)) (a * n)
theorem Polynomial.derivative_C_mul_X {R : Type u} [] (a : R) :
Polynomial.derivative (Polynomial.C a * Polynomial.X) = Polynomial.C a
theorem Polynomial.derivative_C_mul_X_pow {R : Type u} [] (a : R) (n : ) :
Polynomial.derivative (Polynomial.C a * Polynomial.X ^ n) = Polynomial.C (a * n) * Polynomial.X ^ (n - 1)
theorem Polynomial.derivative_C_mul_X_sq {R : Type u} [] (a : R) :
Polynomial.derivative (Polynomial.C a * Polynomial.X ^ 2) = Polynomial.C (a * 2) * Polynomial.X
@[simp]
theorem Polynomial.derivative_X_pow {R : Type u} [] (n : ) :
Polynomial.derivative (Polynomial.X ^ n) = Polynomial.C n * Polynomial.X ^ (n - 1)
theorem Polynomial.derivative_X_sq {R : Type u} [] :
Polynomial.derivative (Polynomial.X ^ 2) = Polynomial.C 2 * Polynomial.X
@[simp]
theorem Polynomial.derivative_C {R : Type u} [] {a : R} :
Polynomial.derivative (Polynomial.C a) = 0
theorem Polynomial.derivative_of_natDegree_zero {R : Type u} [] {p : } (hp : ) :
Polynomial.derivative p = 0
@[simp]
theorem Polynomial.derivative_X {R : Type u} [] :
Polynomial.derivative Polynomial.X = 1
@[simp]
theorem Polynomial.derivative_one {R : Type u} [] :
Polynomial.derivative 1 = 0
theorem Polynomial.derivative_bit0 {R : Type u} [] {a : } :
Polynomial.derivative (bit0 a) = bit0 (Polynomial.derivative a)
theorem Polynomial.derivative_bit1 {R : Type u} [] {a : } :
Polynomial.derivative (bit1 a) = bit0 (Polynomial.derivative a)
theorem Polynomial.derivative_add {R : Type u} [] {f : } {g : } :
Polynomial.derivative (f + g) = Polynomial.derivative f + Polynomial.derivative g
theorem Polynomial.derivative_X_add_C {R : Type u} [] (c : R) :
Polynomial.derivative (Polynomial.X + Polynomial.C c) = 1
theorem Polynomial.derivative_sum {R : Type u} {ι : Type y} [] {s : } {f : ι} :
Polynomial.derivative (Finset.sum s fun b => f b) = Finset.sum s fun b => Polynomial.derivative (f b)
theorem Polynomial.derivative_smul {R : Type u} [] {S : Type u_1} [] [] [] (s : S) (p : ) :
Polynomial.derivative (s p) = s Polynomial.derivative p
@[simp]
theorem Polynomial.iterate_derivative_smul {R : Type u} [] {S : Type u_1} [] [] [] (s : S) (p : ) (k : ) :
@[simp]
theorem Polynomial.iterate_derivative_C_mul {R : Type u} [] (a : R) (p : ) (k : ) :
(Polynomial.derivative)^[k] (Polynomial.C a * p) = Polynomial.C a *
theorem Polynomial.of_mem_support_derivative {R : Type u} [] {p : } {n : } (h : n Polynomial.support (Polynomial.derivative p)) :
n + 1
theorem Polynomial.degree_derivative_lt {R : Type u} [] {p : } (hp : p 0) :
Polynomial.degree (Polynomial.derivative p) <
theorem Polynomial.degree_derivative_le {R : Type u} [] {p : } :
Polynomial.degree (Polynomial.derivative p)
theorem Polynomial.natDegree_derivative_lt {R : Type u} [] {p : } (hp : ) :
Polynomial.natDegree (Polynomial.derivative p) <
theorem Polynomial.natDegree_derivative_le {R : Type u} [] (p : ) :
Polynomial.natDegree (Polynomial.derivative p)
theorem Polynomial.natDegree_iterate_derivative {R : Type u} [] (p : ) (k : ) :
@[simp]
theorem Polynomial.derivative_nat_cast {R : Type u} [] {n : } :
Polynomial.derivative n = 0
@[simp]
theorem Polynomial.derivative_ofNat {R : Type u} [] (n : ) [] :
Polynomial.derivative () = 0
theorem Polynomial.iterate_derivative_eq_zero {R : Type u} [] {p : } {x : } (hx : ) :
@[simp]
theorem Polynomial.iterate_derivative_C {R : Type u} {a : R} [] {k : } (h : 0 < k) :
(Polynomial.derivative)^[k] (Polynomial.C a) = 0
@[simp]
theorem Polynomial.iterate_derivative_one {R : Type u} [] {k : } (h : 0 < k) :
@[simp]
theorem Polynomial.iterate_derivative_X {R : Type u} [] {k : } (h : 1 < k) :
theorem Polynomial.natDegree_eq_zero_of_derivative_eq_zero {R : Type u} [] [] {f : } (h : Polynomial.derivative f = 0) :
theorem Polynomial.eq_C_of_derivative_eq_zero {R : Type u} [] [] {f : } (h : Polynomial.derivative f = 0) :
f = Polynomial.C ()
@[simp]
theorem Polynomial.derivative_mul {R : Type u} [] {f : } {g : } :
Polynomial.derivative (f * g) = Polynomial.derivative f * g + f * Polynomial.derivative g
theorem Polynomial.derivative_eval {R : Type u} [] (p : ) (x : R) :
Polynomial.eval x (Polynomial.derivative p) = Polynomial.sum p fun n a => a * n * x ^ (n - 1)
@[simp]
theorem Polynomial.derivative_map {R : Type u} {S : Type v} [] [] (p : ) (f : R →+* S) :
Polynomial.derivative () = Polynomial.map f (Polynomial.derivative p)
@[simp]
theorem Polynomial.iterate_derivative_map {R : Type u} {S : Type v} [] [] (p : ) (f : R →+* S) (k : ) :
theorem Polynomial.derivative_nat_cast_mul {R : Type u} [] {n : } {f : } :
Polynomial.derivative (n * f) = n * Polynomial.derivative f
@[simp]
theorem Polynomial.iterate_derivative_nat_cast_mul {R : Type u} [] {n : } {k : } {f : } :
theorem Polynomial.mem_support_derivative {R : Type u} [] [] (p : ) (n : ) :
n Polynomial.support (Polynomial.derivative p) n + 1
@[simp]
theorem Polynomial.degree_derivative_eq {R : Type u} [] [] (p : ) (hp : ) :
Polynomial.degree (Polynomial.derivative p) = ↑()
theorem Polynomial.coeff_iterate_derivative {R : Type u} [] {k : } (p : ) (m : ) :
theorem Polynomial.iterate_derivative_mul {R : Type u} [] {n : } (p : ) (q : ) :
theorem Polynomial.derivative_pow_succ {R : Type u} [] (p : ) (n : ) :
Polynomial.derivative (p ^ (n + 1)) = Polynomial.C (n + 1) * p ^ n * Polynomial.derivative p
theorem Polynomial.derivative_pow {R : Type u} [] (p : ) (n : ) :
Polynomial.derivative (p ^ n) = Polynomial.C n * p ^ (n - 1) * Polynomial.derivative p
theorem Polynomial.derivative_sq {R : Type u} [] (p : ) :
Polynomial.derivative (p ^ 2) = Polynomial.C 2 * p * Polynomial.derivative p
theorem Polynomial.dvd_iterate_derivative_pow {R : Type u} [] (f : ) (n : ) {m : } (c : R) (hm : m 0) :
theorem Polynomial.iterate_derivative_X_pow_eq_nat_cast_mul {R : Type u} [] (n : ) (k : ) :
(Polynomial.derivative)^[k] (Polynomial.X ^ n) = ↑() * Polynomial.X ^ (n - k)
theorem Polynomial.iterate_derivative_X_pow_eq_C_mul {R : Type u} [] (n : ) (k : ) :
(Polynomial.derivative)^[k] (Polynomial.X ^ n) = Polynomial.C ↑() * Polynomial.X ^ (n - k)
theorem Polynomial.iterate_derivative_X_pow_eq_smul {R : Type u} [] (n : ) (k : ) :
(Polynomial.derivative)^[k] (Polynomial.X ^ n) = ↑() Polynomial.X ^ (n - k)
theorem Polynomial.derivative_X_add_C_pow {R : Type u} [] (c : R) (m : ) :
Polynomial.derivative ((Polynomial.X + Polynomial.C c) ^ m) = Polynomial.C m * (Polynomial.X + Polynomial.C c) ^ (m - 1)
theorem Polynomial.derivative_X_add_C_sq {R : Type u} [] (c : R) :
Polynomial.derivative ((Polynomial.X + Polynomial.C c) ^ 2) = Polynomial.C 2 * (Polynomial.X + Polynomial.C c)
theorem Polynomial.iterate_derivative_X_add_pow {R : Type u} [] (n : ) (k : ) (c : R) :
(Polynomial.derivative)^[k] ((Polynomial.X + Polynomial.C c) ^ n) = (Polynomial.X + Polynomial.C c) ^ (n - k)
theorem Polynomial.derivative_comp {R : Type u} [] (p : ) (q : ) :
Polynomial.derivative () = Polynomial.derivative q * Polynomial.comp (Polynomial.derivative p) q
theorem Polynomial.derivative_eval₂_C {R : Type u} [] (p : ) (q : ) :
Polynomial.derivative (Polynomial.eval₂ Polynomial.C q p) = Polynomial.eval₂ Polynomial.C q (Polynomial.derivative p) * Polynomial.derivative q

Chain rule for formal derivative of polynomials.

theorem Polynomial.derivative_prod {R : Type u} {ι : Type y} [] {s : } {f : ι} :
Polynomial.derivative () = Multiset.sum (Multiset.map (fun i => Multiset.prod (Multiset.map f ()) * Polynomial.derivative (f i)) s)
theorem Polynomial.derivative_neg {R : Type u} [Ring R] (f : ) :
Polynomial.derivative (-f) = -Polynomial.derivative f
@[simp]
theorem Polynomial.iterate_derivative_neg {R : Type u} [Ring R] {f : } {k : } :
theorem Polynomial.derivative_sub {R : Type u} [Ring R] {f : } {g : } :
Polynomial.derivative (f - g) = Polynomial.derivative f - Polynomial.derivative g
theorem Polynomial.derivative_X_sub_C {R : Type u} [Ring R] (c : R) :
Polynomial.derivative (Polynomial.X - Polynomial.C c) = 1
@[simp]
theorem Polynomial.iterate_derivative_sub {R : Type u} [Ring R] {k : } {f : } {g : } :
@[simp]
theorem Polynomial.derivative_int_cast {R : Type u} [Ring R] {n : } :
Polynomial.derivative n = 0
theorem Polynomial.derivative_int_cast_mul {R : Type u} [Ring R] {n : } {f : } :
Polynomial.derivative (n * f) = n * Polynomial.derivative f
@[simp]
theorem Polynomial.iterate_derivative_int_cast_mul {R : Type u} [Ring R] {n : } {k : } {f : } :
theorem Polynomial.derivative_comp_one_sub_X {R : Type u} [] (p : ) :
Polynomial.derivative (Polynomial.comp p (1 - Polynomial.X)) = -Polynomial.comp (Polynomial.derivative p) (1 - Polynomial.X)
@[simp]
theorem Polynomial.iterate_derivative_comp_one_sub_X {R : Type u} [] (p : ) (k : ) :
(Polynomial.derivative)^[k] (Polynomial.comp p (1 - Polynomial.X)) = (-1) ^ k * Polynomial.comp () (1 - Polynomial.X)
theorem Polynomial.eval_multiset_prod_X_sub_C_derivative {R : Type u} [] {S : } {r : R} (hr : r S) :
Polynomial.eval r (Polynomial.derivative (Multiset.prod (Multiset.map (fun a => Polynomial.X - Polynomial.C a) S))) = Multiset.prod (Multiset.map (fun a => r - a) ())
theorem Polynomial.derivative_X_sub_C_pow {R : Type u} [] (c : R) (m : ) :
Polynomial.derivative ((Polynomial.X - Polynomial.C c) ^ m) = Polynomial.C m * (Polynomial.X - Polynomial.C c) ^ (m - 1)
theorem Polynomial.derivative_X_sub_C_sq {R : Type u} [] (c : R) :
Polynomial.derivative ((Polynomial.X - Polynomial.C c) ^ 2) = Polynomial.C 2 * (Polynomial.X - Polynomial.C c)
theorem Polynomial.iterate_derivative_X_sub_pow {R : Type u} [] (n : ) (k : ) (c : R) :
(Polynomial.derivative)^[k] ((Polynomial.X - Polynomial.C c) ^ n) = (Polynomial.X - Polynomial.C c) ^ (n - k)