mathlib documentation

data.polynomial.derivative

The derivative map on polynomials #

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]
@[simp]
@[simp]
@[simp]
@[simp]
theorem polynomial.derivative_C {R : Type u} [semiring R] {a : R} :
@[simp]
@[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.derivative_smul {R : Type u} [semiring R] {S : Type u_1} [monoid S] [distrib_mul_action S R] [is_scalar_tower 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] [distrib_mul_action S R] [is_scalar_tower S R R] (s : S) (p : polynomial R) (k : ) :
theorem polynomial.of_mem_support_derivative {R : Type u} [semiring R] {p : polynomial R} {n : } (h : n (polynomial.derivative p).support) :
n + 1 p.support
@[simp]
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))
@[simp]
@[simp]
theorem polynomial.derivative_prod {R : Type u} {ι : Type y} [comm_semiring R] {s : multiset ι} {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) :