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

We can't use derivative_mul here because we want to prove this statement also for noncommutative rings.

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 : ) :

The formal derivative of polynomials, as linear homomorphism.

Equations