The derivative map on polynomials

Main definitions

• Polynomial.derivative: The formal derivative of polynomials, expressed as a linear map.
• Polynomial.derivativeFinsupp: Iterated derivatives as a finite support function.

noncomputable def Polynomial.derivative {R : Type u} [Semiring R] : Polynomial R →ₗ[R] Polynomial R

derivative p is the formal derivative of the polynomial p

Equations

• Polynomial.derivative = { toFun := fun (p : Polynomial R) => p.sum fun (n : ℕ) (a : R) => Polynomial.C (a * ↑n) * Polynomial.X ^ (n - 1), map_add' := ⋯, map_smul' := ⋯ }

theorem Polynomial.derivative_apply {R : Type u} [Semiring R] (p : Polynomial R) : derivative p = p.sum fun (n : ℕ) (a : R) => C (a * ↑n) * X ^ (n - 1)

theorem Polynomial.coeff_derivative {R : Type u} [Semiring R] (p : Polynomial R) (n : ℕ) : (derivative p).coeff n = p.coeff (n + 1) * (↑n + 1)

@[simp]

theorem Polynomial.derivative_zero {R : Type u} [Semiring R] : derivative 0 = 0

theorem Polynomial.iterate_derivative_zero {R : Type u} [Semiring R] {k : ℕ} : (⇑derivative)^[k] 0 = 0

theorem Polynomial.derivative_monomial {R : Type u} [Semiring R] (a : R) (n : ℕ) : derivative ((monomial n) a) = (monomial (n - 1)) (a * ↑n)

@[simp]

theorem Polynomial.derivative_monomial_succ {R : Type u} [Semiring R] (a : R) (n : ℕ) : derivative ((monomial (n + 1)) a) = (monomial n) (a * (↑n + 1))

theorem Polynomial.derivative_C_mul_X {R : Type u} [Semiring R] (a : R) : derivative (C a * X) = C a

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

theorem Polynomial.derivative_C_mul_X_sq {R : Type u} [Semiring R] (a : R) : derivative (C a * X ^ 2) = C (a * 2) * X

theorem Polynomial.derivative_X_pow {R : Type u} [Semiring R] (n : ℕ) : derivative (X ^ n) = C ↑n * X ^ (n - 1)

@[simp]

theorem Polynomial.derivative_X_pow_succ {R : Type u} [Semiring R] (n : ℕ) : derivative (X ^ (n + 1)) = C (↑n + 1) * X ^ n

theorem Polynomial.derivative_X_sq {R : Type u} [Semiring R] : derivative (X ^ 2) = C 2 * X

@[simp]

theorem Polynomial.derivative_C {R : Type u} [Semiring R] {a : R} : derivative (C a) = 0

theorem Polynomial.derivative_of_natDegree_zero {R : Type u} [Semiring R] {p : Polynomial R} (hp : p.natDegree = 0) : derivative p = 0

@[simp]

theorem Polynomial.derivative_X {R : Type u} [Semiring R] : derivative X = 1

@[simp]

theorem Polynomial.derivative_one {R : Type u} [Semiring R] : derivative 1 = 0

@[simp]

theorem Polynomial.derivative_add {R : Type u} [Semiring R] {f g : Polynomial R} : derivative (f + g) = derivative f + derivative g

theorem Polynomial.derivative_X_add_C {R : Type u} [Semiring R] (c : R) : derivative (X + C c) = 1

theorem Polynomial.derivative_sum {R : Type u} {ι : Type y} [Semiring R] {s : Finset ι} {f : ι → Polynomial R} : derivative (∑ b ∈ s, f b) = ∑ b ∈ s, derivative (f b)

theorem Polynomial.iterate_derivative_sum {R : Type u} {ι : Type y} [Semiring R] (k : ℕ) (s : Finset ι) (f : ι → Polynomial R) : (⇑derivative)^[k] (∑ b ∈ s, f b) = ∑ b ∈ s, (⇑derivative)^[k] (f b)

theorem Polynomial.derivative_smul {R : Type u} [Semiring R] {S : Type u_1} [SMulZeroClass S R] [IsScalarTower S R R] (s : S) (p : Polynomial R) : derivative (s • p) = s • derivative p

@[simp]

theorem Polynomial.iterate_derivative_smul {R : Type u} [Semiring R] {S : Type u_1} [SMulZeroClass S R] [IsScalarTower S R R] (s : S) (p : Polynomial R) (k : ℕ) : (⇑derivative)^[k] (s • p) = s • (⇑derivative)^[k] p

@[simp]

theorem Polynomial.iterate_derivative_C_mul {R : Type u} [Semiring R] (a : R) (p : Polynomial R) (k : ℕ) : (⇑derivative)^[k] (C a * p) = C a * (⇑derivative)^[k] p

theorem Polynomial.derivative_C_mul {R : Type u} [Semiring R] (a : R) (p : Polynomial R) : derivative (C a * p) = C a * derivative p

theorem Polynomial.of_mem_support_derivative {R : Type u} [Semiring R] {p : Polynomial R} {n : ℕ} (h : n ∈ (derivative p).support) : n + 1 ∈ p.support

theorem Polynomial.degree_derivative_lt {R : Type u} [Semiring R] {p : Polynomial R} (hp : p ≠ 0) : (derivative p).degree < p.degree

theorem Polynomial.degree_derivative_le {R : Type u} [Semiring R] {p : Polynomial R} : (derivative p).degree ≤ p.degree

theorem Polynomial.natDegree_derivative_lt {R : Type u} [Semiring R] {p : Polynomial R} (hp : p.natDegree ≠ 0) : (derivative p).natDegree < p.natDegree

theorem Polynomial.natDegree_derivative_le {R : Type u} [Semiring R] (p : Polynomial R) : (derivative p).natDegree ≤ p.natDegree - 1

theorem Polynomial.natDegree_iterate_derivative {R : Type u} [Semiring R] (p : Polynomial R) (k : ℕ) : ((⇑derivative)^[k] p).natDegree ≤ p.natDegree - k

@[simp]

theorem Polynomial.derivative_natCast {R : Type u} [Semiring R] {n : ℕ} : derivative ↑n = 0

@[simp]

theorem Polynomial.derivative_ofNat {R : Type u} [Semiring R] (n : ℕ) [n.AtLeastTwo] : derivative (OfNat.ofNat n) = 0

theorem Polynomial.iterate_derivative_eq_zero {R : Type u} [Semiring R] {p : Polynomial R} {x : ℕ} (hx : p.natDegree < x) : (⇑derivative)^[x] p = 0

@[simp]

theorem Polynomial.iterate_derivative_C {R : Type u} {a : R} [Semiring R] {k : ℕ} (h : 0 < k) : (⇑derivative)^[k] (C a) = 0

@[simp]

theorem Polynomial.iterate_derivative_one {R : Type u} [Semiring R] {k : ℕ} (h : 0 < k) : (⇑derivative)^[k] 1 = 0

@[simp]

theorem Polynomial.iterate_derivative_X {R : Type u} [Semiring R] {k : ℕ} (h : 1 < k) : (⇑derivative)^[k] X = 0

@[simp]

theorem Polynomial.derivative_mul {R : Type u} [Semiring R] {f g : Polynomial R} : derivative (f * g) = derivative f * g + f * derivative g

theorem Polynomial.derivative_eval {R : Type u} [Semiring R] (p : Polynomial R) (x : R) : eval x (derivative p) = p.sum fun (n : ℕ) (a : R) => a * ↑n * x ^ (n - 1)

@[simp]

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

@[simp]

theorem Polynomial.iterate_derivative_map {R : Type u} {S : Type v} [Semiring R] [Semiring S] (p : Polynomial R) (f : R →+* S) (k : ℕ) : (⇑derivative)^[k] (map f p) = map f ((⇑derivative)^[k] p)

theorem Polynomial.derivative_natCast_mul {R : Type u} [Semiring R] {n : ℕ} {f : Polynomial R} : derivative (↑n * f) = ↑n * derivative f

@[simp]

theorem Polynomial.iterate_derivative_natCast_mul {R : Type u} [Semiring R] {n k : ℕ} {f : Polynomial R} : (⇑derivative)^[k] (↑n * f) = ↑n * (⇑derivative)^[k] f

theorem Polynomial.coeff_iterate_derivative {R : Type u} [Semiring R] {k : ℕ} (p : Polynomial R) (m : ℕ) : ((⇑derivative)^[k] p).coeff m = (m + k).descFactorial k • p.coeff (m + k)

theorem Polynomial.iterate_derivative_eq_sum {R : Type u} [Semiring R] (p : Polynomial R) (k : ℕ) : (⇑derivative)^[k] p = ∑ x ∈ ((⇑derivative)^[k] p).support, C ((x + k).descFactorial k • p.coeff (x + k)) * X ^ x

theorem Polynomial.iterate_derivative_eq_factorial_smul_sum {R : Type u} [Semiring R] (p : Polynomial R) (k : ℕ) : (⇑derivative)^[k] p = k.factorial • ∑ x ∈ ((⇑derivative)^[k] p).support, C ((x + k).choose k • p.coeff (x + k)) * X ^ x

theorem Polynomial.iterate_derivative_mul {R : Type u} [Semiring R] {n : ℕ} (p q : Polynomial R) : (⇑derivative)^[n] (p * q) = ∑ k ∈ Finset.range n.succ, n.choose k • ((⇑derivative)^[n - k] p * (⇑derivative)^[k] q)

noncomputable def Polynomial.derivativeFinsupp {R : Type u} [Semiring R] : Polynomial R →ₗ[R] ℕ →₀ Polynomial R

Iterated derivatives as a finite support function.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem Polynomial.derivativeFinsupp_apply_apply {R : Type u} [Semiring R] (p : Polynomial R) (x✝ : ℕ) : (derivativeFinsupp p) x✝ = (⇑derivative)^[x✝] p

@[simp]

theorem Polynomial.support_derivativeFinsupp_subset_range {R : Type u} [Semiring R] {p : Polynomial R} {n : ℕ} (h : p.natDegree < n) : (derivativeFinsupp p).support ⊆ Finset.range n

@[simp]

theorem Polynomial.derivativeFinsupp_C {R : Type u} [Semiring R] (r : R) : derivativeFinsupp (C r) = Finsupp.single 0 (C r)

@[simp]

theorem Polynomial.derivativeFinsupp_one {R : Type u} [Semiring R] : derivativeFinsupp 1 = Finsupp.single 0 1

@[simp]

theorem Polynomial.derivativeFinsupp_X {R : Type u} [Semiring R] : derivativeFinsupp X = Finsupp.single 0 X + Finsupp.single 1 1

theorem Polynomial.derivativeFinsupp_map {R : Type u} {S : Type v} [Semiring R] [Semiring S] (p : Polynomial R) (f : R →+* S) : derivativeFinsupp (map f p) = Finsupp.mapRange (fun (x : Polynomial R) => map f x) ⋯ (derivativeFinsupp p)

theorem Polynomial.derivativeFinsupp_derivative {R : Type u} [Semiring R] (p : Polynomial R) : derivativeFinsupp (derivative p) = Finsupp.comapDomain Nat.succ (derivativeFinsupp p) ⋯

theorem Polynomial.mem_support_derivative {R : Type u} {n : ℕ} [Semiring R] {p : Polynomial R} [HasUniqueDiv R] : n ∈ (derivative p).support ↔ n + 1 ∈ p.support

@[simp]

theorem Polynomial.degree_derivative {R : Type u} [Semiring R] {p : Polynomial R} [HasUniqueDiv R] (hp : p.natDegree ≠ 0) : (derivative p).degree = ↑(p.natDegree - 1)

@[simp]

theorem Polynomial.natDegree_derivative {R : Type u} [Semiring R] [HasUniqueDiv R] (p : Polynomial R) : (derivative p).natDegree = p.natDegree - 1

@[simp]

theorem Polynomial.derivative_eq_zero {R : Type u} [Semiring R] {p : Polynomial R} [HasUniqueDiv R] : derivative p = 0 ↔ p.natDegree = 0

theorem Polynomial.derivative_ne_zero {R : Type u} [Semiring R] {p : Polynomial R} [HasUniqueDiv R] : derivative p ≠ 0 ↔ p.natDegree ≠ 0

@[simp]

theorem Polynomial.leadingCoeff_derivative {R : Type u} [Semiring R] [HasUniqueDiv R] (p : Polynomial R) : (derivative p).leadingCoeff = p.leadingCoeff * ↑p.natDegree

@[deprecated Polynomial.derivative_eq_zero (since := "2026-06-03")]

theorem Polynomial.natDegree_eq_zero_of_derivative_eq_zero {R : Type u} [Semiring R] {p : Polynomial R} [HasUniqueDiv R] : derivative p = 0 → p.natDegree = 0

Alias of the forward direction of Polynomial.derivative_eq_zero.

theorem Polynomial.eq_C_of_derivative_eq_zero {R : Type u} [Semiring R] {p : Polynomial R} [HasUniqueDiv R] (h : derivative p = 0) : p = C (p.coeff 0)

@[deprecated Polynomial.degree_derivative (since := "2026-06-03")]

theorem Polynomial.degree_derivative_eq {R : Type u} [Semiring R] [HasUniqueDiv R] (p : Polynomial R) (hp : 0 < p.natDegree) : (derivative p).degree = ↑(p.natDegree - 1)

theorem Polynomial.derivative_pow_succ {R : Type u} [CommSemiring R] (p : Polynomial R) (n : ℕ) : derivative (p ^ (n + 1)) = C (↑n + 1) * p ^ n * derivative p

theorem Polynomial.derivative_pow {R : Type u} [CommSemiring R] (p : Polynomial R) (n : ℕ) : derivative (p ^ n) = C ↑n * p ^ (n - 1) * derivative p

theorem Polynomial.derivative_sq {R : Type u} [CommSemiring R] (p : Polynomial R) : derivative (p ^ 2) = C 2 * p * derivative p

theorem Polynomial.pow_sub_one_dvd_derivative_of_pow_dvd {R : Type u} [CommSemiring R] {p q : Polynomial R} {n : ℕ} (dvd : q ^ n ∣ p) : q ^ (n - 1) ∣ derivative p

theorem Polynomial.pow_sub_dvd_iterate_derivative_of_pow_dvd {R : Type u} [CommSemiring R] {p q : Polynomial R} {n : ℕ} (m : ℕ) (dvd : q ^ n ∣ p) : q ^ (n - m) ∣ (⇑derivative)^[m] p

theorem Polynomial.pow_sub_dvd_iterate_derivative_pow {R : Type u} [CommSemiring R] (p : Polynomial R) (n m : ℕ) : p ^ (n - m) ∣ (⇑derivative)^[m] (p ^ n)

theorem Polynomial.dvd_iterate_derivative_pow {R : Type u} [CommSemiring R] (f : Polynomial R) (n : ℕ) {m : ℕ} (c : R) (hm : m ≠ 0) : ↑n ∣ eval c ((⇑derivative)^[m] (f ^ n))

theorem Polynomial.iterate_derivative_X_pow_eq_natCast_mul {R : Type u} [CommSemiring R] (n k : ℕ) : (⇑derivative)^[k] (X ^ n) = ↑(n.descFactorial k) * X ^ (n - k)

theorem Polynomial.iterate_derivative_X_pow_eq_C_mul {R : Type u} [CommSemiring R] (n k : ℕ) : (⇑derivative)^[k] (X ^ n) = C ↑(n.descFactorial k) * X ^ (n - k)

theorem Polynomial.iterate_derivative_X_pow_eq_smul {R : Type u} [CommSemiring R] (n k : ℕ) : (⇑derivative)^[k] (X ^ n) = ↑(n.descFactorial k) • X ^ (n - k)

theorem Polynomial.derivative_X_add_C_pow {R : Type u} [CommSemiring R] (c : R) (m : ℕ) : derivative ((X + C c) ^ m) = C ↑m * (X + C c) ^ (m - 1)

theorem Polynomial.derivative_X_add_C_sq {R : Type u} [CommSemiring R] (c : R) : derivative ((X + C c) ^ 2) = C 2 * (X + C c)

theorem Polynomial.iterate_derivative_X_add_pow {R : Type u} [CommSemiring R] (n k : ℕ) (c : R) : (⇑derivative)^[k] ((X + C c) ^ n) = n.descFactorial k • (X + C c) ^ (n - k)

theorem Polynomial.iterate_derivative_mul_X_pow {R : Type u} [CommSemiring R] (n m : ℕ) (p : Polynomial R) : (⇑derivative)^[n] (p * X ^ m) = ∑ k ∈ Finset.range (min m n).succ, (n.choose k * m.descFactorial k) • ((⇑derivative)^[n - k] p * X ^ (m - k))

theorem Polynomial.iterate_derivative_mul_X {R : Type u} [CommSemiring R] {n : ℕ} (p : Polynomial R) : (⇑derivative)^[n] (p * X) = (⇑derivative)^[n] p * X + n • (⇑derivative)^[n - 1] p

theorem Polynomial.iterate_derivative_derivative_mul_X {R : Type u} [CommSemiring R] {n : ℕ} (p : Polynomial R) : (⇑derivative)^[n] (derivative p * X) = (⇑derivative)^[n + 1] p * X + n • (⇑derivative)^[n] p

theorem Polynomial.iterate_derivative_derivative_mul_X_sq {R : Type u} [CommSemiring R] {n : ℕ} (p : Polynomial R) : (⇑derivative)^[n] ((⇑derivative)^[2] p * X ^ 2) = (⇑derivative)^[n + 2] p * X ^ 2 + (2 * n) • (⇑derivative)^[n + 1] p * X + (n * (n - 1)) • (⇑derivative)^[n] p

theorem Polynomial.derivative_comp {R : Type u} [CommSemiring R] (p q : Polynomial R) : derivative (p.comp q) = derivative q * (derivative p).comp q

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

Chain rule for formal derivative of polynomials.

theorem Polynomial.derivative_prod {R : Type u} {ι : Type y} [CommSemiring R] [DecidableEq ι] {s : Multiset ι} {f : ι → Polynomial R} : derivative (Multiset.map f s).prod = (Multiset.map (fun (i : ι) => (Multiset.map f (s.erase i)).prod * derivative (f i)) s).sum

theorem Polynomial.derivative_prod_finset {R : Type u} {ι : Type y} [CommSemiring R] [DecidableEq ι] {s : Finset ι} {f : ι → Polynomial R} : derivative (∏ b ∈ s, f b) = ∑ a ∈ s, (∏ b ∈ s.erase a, f b) * derivative (f a)

@[simp]

theorem Polynomial.derivative_neg {R : Type u} [Ring R] (f : Polynomial R) : derivative (-f) = -derivative f

theorem Polynomial.iterate_derivative_neg {R : Type u} [Ring R] {f : Polynomial R} {k : ℕ} : (⇑derivative)^[k] (-f) = -(⇑derivative)^[k] f

@[simp]

theorem Polynomial.derivative_sub {R : Type u} [Ring R] {f g : Polynomial R} : derivative (f - g) = derivative f - derivative g

theorem Polynomial.derivative_X_sub_C {R : Type u} [Ring R] (c : R) : derivative (X - C c) = 1

theorem Polynomial.iterate_derivative_sub {R : Type u} [Ring R] {k : ℕ} {f g : Polynomial R} : (⇑derivative)^[k] (f - g) = (⇑derivative)^[k] f - (⇑derivative)^[k] g

@[simp]

theorem Polynomial.derivative_intCast {R : Type u} [Ring R] {n : ℤ} : derivative ↑n = 0

theorem Polynomial.derivative_intCast_mul {R : Type u} [Ring R] {n : ℤ} {f : Polynomial R} : derivative (↑n * f) = ↑n * derivative f

@[simp]

theorem Polynomial.iterate_derivative_intCast_mul {R : Type u} [Ring R] {n : ℤ} {k : ℕ} {f : Polynomial R} : (⇑derivative)^[k] (↑n * f) = ↑n * (⇑derivative)^[k] f

theorem Polynomial.derivative_comp_one_sub_X {R : Type u} [CommRing R] (p : Polynomial R) : derivative (p.comp (1 - X)) = -(derivative p).comp (1 - X)

@[simp]

theorem Polynomial.iterate_derivative_comp_one_sub_X {R : Type u} [CommRing R] (p : Polynomial R) (k : ℕ) : (⇑derivative)^[k] (p.comp (1 - X)) = (-1) ^ k * ((⇑derivative)^[k] p).comp (1 - X)

theorem Polynomial.eval_multiset_prod_X_sub_C_derivative {R : Type u} [CommRing R] [DecidableEq R] {S : Multiset R} {r : R} (hr : r ∈ S) : eval r (derivative (Multiset.map (fun (a : R) => X - C a) S).prod) = (Multiset.map (fun (a : R) => r - a) (S.erase r)).prod

theorem Polynomial.derivative_X_sub_C_pow {R : Type u} [CommRing R] (c : R) (m : ℕ) : derivative ((X - C c) ^ m) = C ↑m * (X - C c) ^ (m - 1)

theorem Polynomial.derivative_X_sub_C_sq {R : Type u} [CommRing R] (c : R) : derivative ((X - C c) ^ 2) = C 2 * (X - C c)

theorem Polynomial.iterate_derivative_X_sub_pow {R : Type u} [CommRing R] (n k : ℕ) (c : R) : (⇑derivative)^[k] ((X - C c) ^ n) = n.descFactorial k • (X - C c) ^ (n - k)

theorem Polynomial.iterate_derivative_X_sub_pow_self {R : Type u} [CommRing R] (n : ℕ) (c : R) : (⇑derivative)^[n] ((X - C c) ^ n) = ↑n.factorial

theorem Polynomial.iterate_derivative_eq_zero_of_degree_lt {R : Type u} [CommRing R] {k : ℕ} {P : Polynomial R} (h : P.degree < ↑k) : (⇑derivative)^[k] P = 0

theorem Polynomial.iterate_derivative_prod_X_sub_C {R : Type u} [CommRing R] {k : ℕ} {S : Finset R} (hk : k ≤ S.card) : (⇑derivative)^[k] (∏ a ∈ S, (X - C a)) = ↑k.factorial * ∑ T ∈ Finset.powersetCard (S.card - k) S, ∏ a ∈ T, (X - C a)

@[simp]

theorem Polynomial.dvd_derivative_iff {R : Type u} [Semiring R] [NoZeroDivisors R] {P : Polynomial R} : P ∣ derivative P ↔ derivative P = 0

theorem Polynomial.derivative_pow_eq_zero {R : Type u} [CommSemiring R] [NoZeroDivisors R] {n : ℕ} (chn : ↑n ≠ 0) {a : Polynomial R} : derivative (a ^ n) = 0 ↔ derivative a = 0