mathlib documentation

data.polynomial.derivative

The derivative map on polynomials

Main definitions

derivative p is the formal derivative of the polynomial p

Equations
theorem polynomial.derivative_apply {R : Type u} [semiring R] (p : polynomial R) :

theorem polynomial.coeff_derivative {R : Type u} [semiring R] (p : polynomial R) (n : ) :
(polynomial.derivative p).coeff n = (p.coeff (n + 1)) * (n + 1)

@[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 (∑ (b : ι) in s, f b) = ∑ (b : ι) in s, polynomial.derivative (f b)

@[simp]

theorem polynomial.derivative_eval {R : Type u} [comm_semiring R] (p : polynomial R) (x : R) :
polynomial.eval x (polynomial.derivative p) = finsupp.sum p (λ (n : ) (a : R), (a * n) * x ^ (n - 1))

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

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