mathlib documentation

data.polynomial.iterated_deriv

Theory of iterated derivative

We define and prove some lemmas about iterated (formal) derivative for polynomials over a semiring.

def polynomial.iterated_deriv {R : Type u} [semiring R] (f : polynomial R) (n : ) :

iterated_deriv f n is the n-th formal derivative of the polynomial f

Equations
@[simp]
theorem polynomial.iterated_deriv_zero_right {R : Type u} [semiring R] (f : polynomial R) :

theorem polynomial.iterated_deriv_succ {R : Type u} [semiring R] (f : polynomial R) (n : ) :

@[simp]
theorem polynomial.iterated_deriv_zero_left {R : Type u} [semiring R] (n : ) :

@[simp]
theorem polynomial.iterated_deriv_add {R : Type u} [semiring R] (p q : polynomial R) (n : ) :

@[simp]
theorem polynomial.iterated_deriv_smul {R : Type u} [semiring R] (r : R) (p : polynomial R) (n : ) :

@[simp]
theorem polynomial.iterated_deriv_X {R : Type u} [semiring R] (n : ) (h : 1 < n) :

@[simp]
theorem polynomial.iterated_deriv_C {R : Type u} [semiring R] (r : R) (n : ) (h : 0 < n) :

@[simp]
theorem polynomial.iterated_deriv_one_zero {R : Type u} [semiring R] :

@[simp]
theorem polynomial.iterated_deriv_one {R : Type u} [semiring R] (n : ) :
0 < n1.iterated_deriv n = 0

@[simp]
theorem polynomial.iterated_deriv_neg {R : Type u} [ring R] (p : polynomial R) (n : ) :

@[simp]
theorem polynomial.iterated_deriv_sub {R : Type u} [ring R] (p q : polynomial R) (n : ) :

theorem polynomial.coeff_iterated_deriv_as_prod_Ico {R : Type u} [comm_semiring R] (f : polynomial R) (k m : ) :
(f.iterated_deriv k).coeff m = (∏ (i : ) in finset.Ico m.succ (m + k.succ), i) * f.coeff (m + k)

theorem polynomial.coeff_iterated_deriv_as_prod_range {R : Type u} [comm_semiring R] (f : polynomial R) (k m : ) :
(f.iterated_deriv k).coeff m = (f.coeff (m + k)) * ∏ (i : ) in finset.range k, (m + k - i)

theorem polynomial.iterated_deriv_mul {R : Type u} [comm_semiring R] (p q : polynomial R) (n : ) :