mathlib documentation

data.polynomial.derivative

Theory of univariate polynomials

source
def polynomial.derivative {R : Type u} [semiring R] :
polynomial R → polynomial R

derivative p is the formal derivative of the polynomial p

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

source
@[simp]
theorem polynomial.derivative_zero {R : Type u} [semiring R] :
0.derivative = 0

source
theorem polynomial.derivative_monomial {R : Type u} [semiring R] (a : R) (n : ℕ) :
(⇑(polynomial.monomial n) a).derivative = ⇑(polynomial.monomial (n - 1)) (a * ↑n)

source
theorem polynomial.derivative_C_mul_X_pow {R : Type u} [semiring R] (a : R) (n : ℕ) :
((⇑polynomial.C a) * polynomial.X ^ n).derivative = (⇑polynomial.C (a * ↑n)) * polynomial.X ^ (n - 1)

source
@[simp]
theorem polynomial.derivative_C {R : Type u} [semiring R] {a : R} :
(⇑polynomial.C a).derivative = 0

source
@[simp]
theorem polynomial.derivative_X {R : Type u} [semiring R] :
polynomial.X.derivative = 1

source
@[simp]
theorem polynomial.derivative_one {R : Type u} [semiring R] :
1.derivative = 0

source
@[simp]
theorem polynomial.derivative_add {R : Type u} [semiring R] {f g : polynomial R} :
(f + g).derivative = f.derivative + g.derivative

source
def polynomial.derivative_hom (R : Type u_1) [semiring R] :
polynomial R →+ polynomial R

The formal derivative of polynomials, as additive homomorphism.

Equations
source
@[simp]
theorem polynomial.derivative_neg {R : Type u_1} [ring R] (f : polynomial R) :
(-f).derivative = -f.derivative

source
@[simp]
theorem polynomial.derivative_sub {R : Type u_1} [ring R] (f g : polynomial R) :
(f - g).derivative = f.derivative - g.derivative

source
@[instance]
def polynomial.is_add_monoid_hom {R : Type u} [semiring R] :
is_add_monoid_hom polynomial.derivative

source
@[simp]
theorem polynomial.derivative_sum {R : Type u} {ι : Type y} [semiring R] {s : finset ι} {f : ι → polynomial R} :
(∑ (b : ι) in s, f b).derivative = ∑ (b : ι) in s, (f b).derivative

source
@[simp]
theorem polynomial.derivative_smul {R : Type u} [semiring R] (r : R) (p : polynomial R) :
(r • p).derivative = r • p.derivative

source
@[simp]
theorem polynomial.derivative_mul {R : Type u} [comm_semiring R] {f g : polynomial R} :
(f * g).derivative = (f.derivative) * g + f * g.derivative

source
theorem polynomial.derivative_pow_succ {R : Type u} [comm_semiring R] (p : polynomial R) (n : ℕ) :
(p ^ (n + 1)).derivative = ((↑n + 1) * p ^ n) * p.derivative

source
theorem polynomial.derivative_pow {R : Type u} [comm_semiring R] (p : polynomial R) (n : ℕ) :
(p ^ n).derivative = ((↑n) * p ^ (n - 1)) * p.derivative

source
theorem polynomial.derivative_map {R : Type u} {S : Type v} [comm_semiring R] [comm_semiring S] (p : polynomial R) (f : R →+* S) :
(polynomial.map f p).derivative = polynomial.map f p.derivative

source
theorem polynomial.derivative_eval₂_C {R : Type u} [comm_semiring R] (p q : polynomial R) :
(polynomial.eval₂ polynomial.C q p).derivative = (polynomial.eval₂ polynomial.C q p.derivative) * q.derivative

Chain rule for formal derivative of polynomials.

source
theorem polynomial.of_mem_support_derivative {R : Type u} [comm_semiring R] {p : polynomial R} {n : ℕ} :
n ∈ p.derivative.support → n + 1 ∈ p.support

source
theorem polynomial.degree_derivative_lt {R : Type u} [comm_semiring R] {p : polynomial R} :
p ≠ 0 → p.derivative.degree < p.degree

source
theorem polynomial.nat_degree_derivative_lt {R : Type u} [comm_semiring R] {p : polynomial R} :
p.derivative ≠ 0 → p.derivative.nat_degree < p.nat_degree

source
theorem polynomial.degree_derivative_le {R : Type u} [comm_semiring R] {p : polynomial R} :
p.derivative.degree ≤ p.degree

source
def polynomial.derivative_lhom (R : Type u_1) [comm_ring R] :
polynomial R →ₗ[R] polynomial R

The formal derivative of polynomials, as linear homomorphism.

Equations
source
theorem polynomial.mem_support_derivative {R : Type u} [integral_domain R] [char_zero R] (p : polynomial R) (n : ℕ) :
n ∈ p.derivative.support ↔ n + 1 ∈ p.support

source
@[simp]
theorem polynomial.degree_derivative_eq {R : Type u} [integral_domain R] [char_zero R] (p : polynomial R) :
0 < p.nat_degree → p.derivative.degree = ↑(p.nat_degree - 1)

source
theorem polynomial.nat_degree_eq_zero_of_derivative_eq_zero {R : Type u} [integral_domain R] [char_zero R] {f : polynomial R} :
f.derivative = 0 → f.nat_degree = 0