doc-next-gen

Mathlib.Algebra.Polynomial.Derivative

Module docstring

{"# 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.

"}

Polynomial.derivative definition
: R[X] →ₗ[R] R[X]
Full source 
/-- `derivative p` is the formal derivative of the polynomial `p` -/
def derivative : R[X]R[X] →ₗ[R] R[X] where
  toFun p := p.sum fun n a => C (a * n) * X ^ (n - 1)
  map_add' p q := by
    rw [sum_add_index] <;>
      simp only [add_mul, forall_const, RingHom.map_add, eq_self_iff_true, zero_mul,
        RingHom.map_zero]
  map_smul' a p := by
    dsimp; rw [sum_smul_index] <;>
      simp only [mul_sum, ← C_mul', mul_assoc, coeff_C_mul, RingHom.map_mul, forall_const, zero_mul,
        RingHom.map_zero, sum]
Formal derivative of polynomials
Informal description
The formal derivative of a polynomial $p \in R[X]$ is the linear map $D \colon R[X] \to R[X]$ defined by: \[ D(p) = \sum_{n} (a_n \cdot n) X^{n-1} \] where $p = \sum_n a_n X^n$ is the expansion of $p$. This derivative satisfies the usual linearity properties: 1. Additivity: $D(p + q) = D(p) + D(q)$ for all $p, q \in R[X]$ 2. Scalar multiplication: $D(a \cdot p) = a \cdot D(p)$ for all $a \in R$ and $p \in R[X]$
Polynomial.derivative_apply theorem
(p : R[X]) : derivative p = p.sum fun n a => C (a * n) * X ^ (n - 1)
Full source 
theorem derivative_apply (p : R[X]) : derivative p = p.sum fun n a => C (a * n) * X ^ (n - 1) :=
  rfl
Explicit Formula for Polynomial Derivative
Informal description
For any polynomial $p \in R[X]$, the formal derivative $D(p)$ is given by: \[ D(p) = \sum_{n} (a_n \cdot n) X^{n-1} \] where $p = \sum_n a_n X^n$ is the expansion of $p$ and $a_n$ are its coefficients.
Polynomial.coeff_derivative theorem
(p : R[X]) (n : ℕ) : coeff (derivative p) n = coeff p (n + 1) * (n + 1)
Full source 
theorem coeff_derivative (p : R[X]) (n : ℕ) :
    coeff (derivative p) n = coeff p (n + 1) * (n + 1) := by
  rw [derivative_apply]
  simp only [coeff_X_pow, coeff_sum, coeff_C_mul]
  rw [sum, Finset.sum_eq_single (n + 1)]
  · simp only [Nat.add_succ_sub_one, add_zero, mul_one, if_true, eq_self_iff_true]; norm_cast
  · intro b
    cases b
    · intros
      rw [Nat.cast_zero, mul_zero, zero_mul]
    · intro _ H
      rw [Nat.add_one_sub_one, if_neg (mt (congr_arg Nat.succ) H.symm), mul_zero]
  · rw [if_pos (add_tsub_cancel_right n 1).symm, mul_one, Nat.cast_add, Nat.cast_one,
      mem_support_iff]
    intro h
    push_neg at h
    simp [h]
Coefficient Formula for Polynomial Derivative: $\text{coeff}(D(p), n) = (n+1) \cdot \text{coeff}(p, n+1)$
Informal description
For any polynomial $p \in R[X]$ and natural number $n$, the coefficient of $X^n$ in the formal derivative $D(p)$ is equal to the coefficient of $X^{n+1}$ in $p$ multiplied by $(n+1)$, i.e., $$\text{coeff}(D(p), n) = \text{coeff}(p, n+1) \cdot (n+1).$$
Polynomial.derivative_zero theorem
: derivative (0 : R[X]) = 0
Full source 
@[simp]
theorem derivative_zero : derivative (0 : R[X]) = 0 :=
  derivative.map_zero
Derivative of Zero Polynomial is Zero
Informal description
The formal derivative of the zero polynomial in $R[X]$ is the zero polynomial, i.e., $D(0) = 0$.
Polynomial.iterate_derivative_zero theorem
{k : ℕ} : derivative^[k] (0 : R[X]) = 0
Full source 
theorem iterate_derivative_zero {k : ℕ} : derivativederivative^[k] (0 : R[X]) = 0 :=
  iterate_map_zero derivative k
$k$-th Derivative of Zero Polynomial is Zero
Informal description
For any natural number $k$, the $k$-th iterate of the formal derivative operator applied to the zero polynomial $0 \in R[X]$ yields the zero polynomial, i.e., $D^k(0) = 0$.
Polynomial.derivative_monomial theorem
(a : R) (n : ℕ) : derivative (monomial n a) = monomial (n - 1) (a * n)
Full source 
theorem derivative_monomial (a : R) (n : ℕ) :
    derivative (monomial n a) = monomial (n - 1) (a * n) := by
  rw [derivative_apply, sum_monomial_index, C_mul_X_pow_eq_monomial]
  simp
Derivative of Monomial: $\frac{d}{dX}(aX^n) = a \cdot n X^{n-1}$
Informal description
For any coefficient $a$ in a semiring $R$ and any natural number $n$, the derivative of the monomial $aX^n$ is given by $a \cdot n X^{n-1}$. In other words, the formal derivative satisfies: \[ \frac{d}{dX}(aX^n) = a \cdot n X^{n-1}. \]
Polynomial.derivative_monomial_succ theorem
(a : R) (n : ℕ) : derivative (monomial (n + 1) a) = monomial n (a * (n + 1))
Full source 
@[simp]
theorem derivative_monomial_succ (a : R) (n : ℕ) :
    derivative (monomial (n + 1) a) = monomial n (a * (n + 1)) := by
  rw [derivative_monomial, add_tsub_cancel_right, Nat.cast_add, Nat.cast_one]
Derivative of Monomial: $\frac{d}{dX}(aX^{n+1}) = a(n+1)X^n$
Informal description
For any coefficient $a$ in a semiring $R$ and any natural number $n$, the derivative of the monomial $aX^{n+1}$ is given by $a(n+1)X^n$. In other words, the formal derivative satisfies: \[ \frac{d}{dX}(aX^{n+1}) = a(n+1)X^n. \]
Polynomial.derivative_C_mul_X theorem
(a : R) : derivative (C a * X) = C a
Full source 
theorem derivative_C_mul_X (a : R) : derivative (C a * X) = C a := by
  simp [C_mul_X_eq_monomial, derivative_monomial, Nat.cast_one, mul_one]
Derivative of Linear Polynomial: $\frac{d}{dX}(a X) = a$
Informal description
For any element $a$ in a semiring $R$, the derivative of the polynomial $a X$ is equal to the constant polynomial $a$, i.e., \[ \frac{d}{dX}(a X) = a. \]
Polynomial.derivative_C_mul_X_pow theorem
(a : R) (n : ℕ) : derivative (C a * X ^ n) = C (a * n) * X ^ (n - 1)
Full source 
theorem derivative_C_mul_X_pow (a : R) (n : ℕ) :
    derivative (C a * X ^ n) = C (a * n) * X ^ (n - 1) := by
  rw [C_mul_X_pow_eq_monomial, C_mul_X_pow_eq_monomial, derivative_monomial]
Derivative of monomial: $\frac{d}{dX}(a X^n) = a \cdot n X^{n-1}$
Informal description
For any coefficient $a$ in a semiring $R$ and any natural number $n$, the derivative of the polynomial $a X^n$ is given by $a \cdot n X^{n-1}$. In other words, the formal derivative satisfies: \[ \frac{d}{dX}(a X^n) = a \cdot n X^{n-1}. \]
Polynomial.derivative_C_mul_X_sq theorem
(a : R) : derivative (C a * X ^ 2) = C (a * 2) * X
Full source 
theorem derivative_C_mul_X_sq (a : R) : derivative (C a * X ^ 2) = C (a * 2) * X := by
  rw [derivative_C_mul_X_pow, Nat.cast_two, pow_one]
Derivative of quadratic monomial: $\frac{d}{dX}(a X^2) = 2a X$
Informal description
For any coefficient $a$ in a semiring $R$, the derivative of the quadratic monomial $a X^2$ is given by $2a X$. In other words, the formal derivative satisfies: \[ \frac{d}{dX}(a X^2) = 2a X. \]
Polynomial.derivative_X_pow theorem
(n : ℕ) : derivative (X ^ n : R[X]) = C (n : R) * X ^ (n - 1)
Full source 
theorem derivative_X_pow (n : ℕ) : derivative (X ^ n : R[X]) = C (n : R) * X ^ (n - 1) := by
  convert derivative_C_mul_X_pow (1 : R) n <;> simp
Derivative of $X^n$: $\frac{d}{dX}(X^n) = n X^{n-1}$
Informal description
For any natural number $n$, the derivative of the monomial $X^n$ in the polynomial ring $R[X]$ is given by $n X^{n-1}$. That is, \[ \frac{d}{dX}(X^n) = n X^{n-1}. \]
Polynomial.derivative_X_pow_succ theorem
(n : ℕ) : derivative (X ^ (n + 1) : R[X]) = C (n + 1 : R) * X ^ n
Full source 
@[simp]
theorem derivative_X_pow_succ (n : ℕ) :
    derivative (X ^ (n + 1) : R[X]) = C (n + 1 : R) * X ^ n := by
  simp [derivative_X_pow]
Derivative of $X^{n+1}$: $\frac{d}{dX}(X^{n+1}) = (n+1) X^n$
Informal description
For any natural number $n$, the derivative of the monomial $X^{n+1}$ in the polynomial ring $R[X]$ is given by $(n+1) X^n$. That is, \[ \frac{d}{dX}(X^{n+1}) = (n+1) X^n. \]
Polynomial.derivative_X_sq theorem
: derivative (X ^ 2 : R[X]) = C 2 * X
Full source 
theorem derivative_X_sq : derivative (X ^ 2 : R[X]) = C 2 * X := by
  rw [derivative_X_pow, Nat.cast_two, pow_one]
Derivative of $X^2$: $\frac{d}{dX}(X^2) = 2X$
Informal description
The formal derivative of the monomial $X^2$ in the polynomial ring $R[X]$ is $2X$, i.e., \[ \frac{d}{dX}(X^2) = 2X. \]
Polynomial.derivative_C theorem
{a : R} : derivative (C a) = 0
Full source 
@[simp]
theorem derivative_C {a : R} : derivative (C a) = 0 := by simp [derivative_apply]
Derivative of a Constant Polynomial is Zero
Informal description
For any element $a$ in a semiring $R$, the formal derivative of the constant polynomial $C(a) \in R[X]$ is the zero polynomial, i.e., $\frac{d}{dX} a = 0$.
Polynomial.derivative_of_natDegree_zero theorem
{p : R[X]} (hp : p.natDegree = 0) : derivative p = 0
Full source 
theorem derivative_of_natDegree_zero {p : R[X]} (hp : p.natDegree = 0) : derivative p = 0 := by
  rw [eq_C_of_natDegree_eq_zero hp, derivative_C]
Derivative of a Constant Polynomial is Zero
Informal description
For any polynomial $p \in R[X]$ with natural degree zero (i.e., $p$ is a constant polynomial), its formal derivative is the zero polynomial, i.e., $\frac{d}{dX} p = 0$.
Polynomial.derivative_X theorem
: derivative (X : R[X]) = 1
Full source 
@[simp]
theorem derivative_X : derivative (X : R[X]) = 1 :=
  (derivative_monomial _ _).trans <| by simp
Derivative of the Polynomial Variable: $\frac{d}{dX} X = 1$
Informal description
The formal derivative of the polynomial variable $X$ in the polynomial ring $R[X]$ is equal to the constant polynomial $1$, i.e., $\frac{d}{dX} X = 1$.
Polynomial.derivative_one theorem
: derivative (1 : R[X]) = 0
Full source 
@[simp]
theorem derivative_one : derivative (1 : R[X]) = 0 :=
  derivative_C
Derivative of the Constant One Polynomial is Zero
Informal description
The formal derivative of the constant polynomial $1 \in R[X]$ is the zero polynomial, i.e., $\frac{d}{dX} 1 = 0$.
Polynomial.derivative_add theorem
{f g : R[X]} : derivative (f + g) = derivative f + derivative g
Full source 
@[simp]
theorem derivative_add {f g : R[X]} : derivative (f + g) = derivative f + derivative g :=
  derivative.map_add f g
Additivity of Polynomial Derivative: $\frac{d}{dX}(f + g) = \frac{d}{dX}f + \frac{d}{dX}g$
Informal description
For any two polynomials $f, g \in R[X]$ over a semiring $R$, the derivative of their sum is equal to the sum of their derivatives, i.e., \[ \frac{d}{dX}(f + g) = \frac{d}{dX}f + \frac{d}{dX}g. \]
Polynomial.derivative_X_add_C theorem
(c : R) : derivative (X + C c) = 1
Full source 
theorem derivative_X_add_C (c : R) : derivative (X + C c) = 1 := by
  rw [derivative_add, derivative_X, derivative_C, add_zero]
Derivative of Linear Polynomial: $\frac{d}{dX}(X + c) = 1$
Informal description
For any element $c$ in a semiring $R$, the formal derivative of the polynomial $X + c$ in $R[X]$ is equal to the constant polynomial $1$, i.e., \[ \frac{d}{dX}(X + c) = 1. \]
Polynomial.derivative_sum theorem
{s : Finset ι} {f : ι → R[X]} : derivative (∑ b ∈ s, f b) = ∑ b ∈ s, derivative (f b)
Full source 
theorem derivative_sum {s : Finset ι} {f : ι → R[X]} :
    derivative (∑ b ∈ s, f b) = ∑ b ∈ s, derivative (f b) :=
  map_sum ..
Linearity of Polynomial Derivative over Finite Sums
Informal description
For any finite set $s$ and any family of polynomials $(f_b)_{b \in s}$ in $R[X]$, the derivative of the sum $\sum_{b \in s} f_b$ is equal to the sum of the derivatives $\sum_{b \in s} \frac{d}{dX} f_b$.
Polynomial.iterate_derivative_sum theorem
(k : ℕ) (s : Finset ι) (f : ι → R[X]) : derivative^[k] (∑ b ∈ s, f b) = ∑ b ∈ s, derivative^[k] (f b)
Full source 
theorem iterate_derivative_sum (k : ℕ) (s : Finset ι) (f : ι → R[X]) :
    derivativederivative^[k] (∑ b ∈ s, f b) = ∑ b ∈ s, derivative^[k] (f b) := by
  simp_rw [← Module.End.pow_apply, map_sum]
Iterated Derivative Distributes over Finite Sum of Polynomials
Informal description
For any natural number $k$, any finite set $s$, and any family of polynomials $(f_b)_{b \in s}$ in $R[X]$, the $k$-th iterate of the derivative operator applied to the sum $\sum_{b \in s} f_b$ equals the sum of the $k$-th iterated derivatives of the individual polynomials, i.e., \[ \frac{d^k}{dX^k} \left( \sum_{b \in s} f_b \right) = \sum_{b \in s} \frac{d^k}{dX^k} f_b. \]
Polynomial.derivative_smul theorem
{S : Type*} [SMulZeroClass S R] [IsScalarTower S R R] (s : S) (p : R[X]) : derivative (s • p) = s • derivative p
Full source 
theorem derivative_smul {S : Type*} [SMulZeroClass S R] [IsScalarTower S R R] (s : S)
    (p : R[X]) : derivative (s • p) = s • derivative p :=
  derivative.map_smul_of_tower s p
Derivative of Scalar Multiple of Polynomial: $\frac{d}{dX}(s \cdot p) = s \cdot \frac{d}{dX} p$
Informal description
Let $R$ be a semiring and $S$ a type with a scalar multiplication action on $R$ that preserves zero and forms a scalar tower over $R$. For any scalar $s \in S$ and polynomial $p \in R[X]$, the derivative of the scalar multiple $s \cdot p$ is equal to the scalar multiple of the derivative, i.e., \[ \frac{d}{dX}(s \cdot p) = s \cdot \frac{d}{dX} p. \]
Polynomial.iterate_derivative_smul theorem
{S : Type*} [SMulZeroClass S R] [IsScalarTower S R R] (s : S) (p : R[X]) (k : ℕ) : derivative^[k] (s • p) = s • derivative^[k] p
Full source 
@[simp]
theorem iterate_derivative_smul {S : Type*} [SMulZeroClass S R] [IsScalarTower S R R]
    (s : S) (p : R[X]) (k : ℕ) : derivativederivative^[k] (s • p) = s • derivativederivative^[k] p := by
  induction k generalizing p with
  | zero => simp
  | succ k ih => simp [ih]
Iterated Derivative Commutes with Scalar Multiplication: $D^k(s \cdot p) = s \cdot D^k(p)$
Informal description
Let $R$ be a semiring and $S$ a type with a scalar multiplication action on $R$ that preserves zero and forms a scalar tower over $R$. For any scalar $s \in S$, polynomial $p \in R[X]$, and natural number $k$, the $k$-th iterate of the formal derivative of the scalar multiple $s \cdot p$ is equal to the scalar multiple of the $k$-th iterate of the derivative of $p$, i.e., \[ D^k(s \cdot p) = s \cdot D^k(p), \] where $D$ denotes the formal derivative operator on $R[X]$.
Polynomial.iterate_derivative_C_mul theorem
(a : R) (p : R[X]) (k : ℕ) : derivative^[k] (C a * p) = C a * derivative^[k] p
Full source 
@[simp]
theorem iterate_derivative_C_mul (a : R) (p : R[X]) (k : ℕ) :
    derivativederivative^[k] (C a * p) = C a * derivativederivative^[k] p := by
  simp_rw [← smul_eq_C_mul, iterate_derivative_smul]
Iterated Derivative of Scalar Multiple: $D^k(a \cdot p) = a \cdot D^k(p)$
Informal description
For any element $a$ in a semiring $R$, any polynomial $p \in R[X]$, and any natural number $k$, the $k$-th iterate of the formal derivative of the product of the constant polynomial $a$ and $p$ is equal to the product of the constant polynomial $a$ and the $k$-th iterate of the derivative of $p$, i.e., \[ D^k(a \cdot p) = a \cdot D^k(p), \] where $D$ denotes the formal derivative operator on $R[X]$.
Polynomial.derivative_C_mul theorem
(a : R) (p : R[X]) : derivative (C a * p) = C a * derivative p
Full source 
theorem derivative_C_mul (a : R) (p : R[X]) :
    derivative (C a * p) = C a * derivative p := iterate_derivative_C_mul _ _ 1
Derivative of Scalar Multiple: $D(a \cdot p) = a \cdot D(p)$
Informal description
For any element $a$ in a semiring $R$ and any polynomial $p \in R[X]$, the derivative of the product of the constant polynomial $a$ and $p$ is equal to the product of the constant polynomial $a$ and the derivative of $p$, i.e., \[ D(a \cdot p) = a \cdot D(p), \] where $D$ denotes the formal derivative operator on $R[X]$.
Polynomial.of_mem_support_derivative theorem
{p : R[X]} {n : ℕ} (h : n ∈ p.derivative.support) : n + 1 ∈ p.support
Full source 
theorem of_mem_support_derivative {p : R[X]} {n : ℕ} (h : n ∈ p.derivative.support) :
    n + 1 ∈ p.support :=
  mem_support_iff.2 fun h1 : p.coeff (n + 1) = 0 =>
    mem_support_iff.1 h <| show p.derivative.coeff n = 0 by rw [coeff_derivative, h1, zero_mul]
Support Inclusion: $n \in \text{supp}(p') \Rightarrow n+1 \in \text{supp}(p)$
Informal description
For any polynomial $p \in R[X]$ and natural number $n$, if $n$ is in the support of the derivative $p'$ (i.e., the coefficient of $X^n$ in $p'$ is nonzero), then $n + 1$ is in the support of $p$ (i.e., the coefficient of $X^{n+1}$ in $p$ is nonzero).
Polynomial.degree_derivative_lt theorem
{p : R[X]} (hp : p ≠ 0) : p.derivative.degree < p.degree
Full source 
theorem degree_derivative_lt {p : R[X]} (hp : p ≠ 0) : p.derivative.degree < p.degree :=
  (Finset.sup_lt_iff <| bot_lt_iff_ne_bot.2 <| mt degree_eq_bot.1 hp).2 fun n hp =>
    lt_of_lt_of_le (WithBot.coe_lt_coe.2 n.lt_succ_self) <|
      Finset.le_sup <| of_mem_support_derivative hp
Degree Strict Inequality for Polynomial Derivatives: $\deg(p') < \deg(p)$ for $p \neq 0$
Informal description
For any nonzero polynomial $p \in R[X]$, the degree of its formal derivative $p'$ is strictly less than the degree of $p$, i.e., $\deg(p') < \deg(p)$.
Polynomial.degree_derivative_le theorem
{p : R[X]} : p.derivative.degree ≤ p.degree
Full source 
theorem degree_derivative_le {p : R[X]} : p.derivative.degree ≤ p.degree :=
  letI := Classical.decEq R
  if H : p = 0 then le_of_eq <| by rw [H, derivative_zero] else (degree_derivative_lt H).le
Degree Non-Increasing Property of Polynomial Derivatives: $\deg(p') \leq \deg(p)$
Informal description
For any polynomial $p \in R[X]$, the degree of its formal derivative $p'$ is less than or equal to the degree of $p$, i.e., $\deg(p') \leq \deg(p)$.
Polynomial.natDegree_derivative_lt theorem
{p : R[X]} (hp : p.natDegree ≠ 0) : p.derivative.natDegree < p.natDegree
Full source 
theorem natDegree_derivative_lt {p : R[X]} (hp : p.natDegree ≠ 0) :
    p.derivative.natDegree < p.natDegree := by
  rcases eq_or_ne (derivative p) 0 with hp' | hp'
  · rw [hp', Polynomial.natDegree_zero]
    exact hp.bot_lt
  · rw [natDegree_lt_natDegree_iff hp']
    exact degree_derivative_lt fun h => hp (h.symm ▸ natDegree_zero)
Strict Natural Degree Inequality for Polynomial Derivatives: $\text{natDegree}(p') < \text{natDegree}(p)$ when $\text{natDegree}(p) \neq 0$
Informal description
For any polynomial $p \in R[X]$ with nonzero natural degree, the natural degree of its formal derivative $p'$ is strictly less than the natural degree of $p$, i.e., $\text{natDegree}(p') < \text{natDegree}(p)$.
Polynomial.natDegree_derivative_le theorem
(p : R[X]) : p.derivative.natDegree ≤ p.natDegree - 1
Full source 
theorem natDegree_derivative_le (p : R[X]) : p.derivative.natDegree ≤ p.natDegree - 1 := by
  by_cases p0 : p.natDegree = 0
  · simp [p0, derivative_of_natDegree_zero]
  · exact Nat.le_sub_one_of_lt (natDegree_derivative_lt p0)
Natural Degree Bound for Polynomial Derivatives: $\text{natDegree}(p') \leq \text{natDegree}(p) - 1$
Informal description
For any polynomial $p \in R[X]$, the natural degree of its derivative $p'$ satisfies $\text{natDegree}(p') \leq \text{natDegree}(p) - 1$.
Polynomial.natDegree_iterate_derivative theorem
(p : R[X]) (k : ℕ) : (derivative^[k] p).natDegree ≤ p.natDegree - k
Full source 
theorem natDegree_iterate_derivative (p : R[X]) (k : ℕ) :
    (derivativederivative^[k] p).natDegree ≤ p.natDegree - k := by
  induction k with
  | zero => rw [Function.iterate_zero_apply, Nat.sub_zero]
  | succ d hd =>
      rw [Function.iterate_succ_apply', Nat.sub_succ']
      exact (natDegree_derivative_le _).trans <| Nat.sub_le_sub_right hd 1
Degree Bound for Iterated Derivatives: $\text{natDegree}(p^{(k)}) \leq \text{natDegree}(p) - k$
Informal description
For any polynomial $p \in R[X]$ and natural number $k$, the natural degree of the $k$-th iterate of the derivative of $p$ satisfies $\text{natDegree}(p^{(k)}) \leq \text{natDegree}(p) - k$.
Polynomial.derivative_natCast theorem
{n : ℕ} : derivative (n : R[X]) = 0
Full source 
@[simp]
theorem derivative_natCast {n : ℕ} : derivative (n : R[X]) = 0 := by
  rw [← map_natCast C n]
  exact derivative_C
Derivative of Natural Number Constant Polynomial is Zero
Informal description
For any natural number $n$, the formal derivative of the constant polynomial $n$ in the polynomial ring $R[X]$ is the zero polynomial, i.e., $\frac{d}{dX} n = 0$.
Polynomial.derivative_ofNat theorem
(n : ℕ) [n.AtLeastTwo] : derivative (ofNat(n) : R[X]) = 0
Full source 
@[simp]
theorem derivative_ofNat (n : ℕ) [n.AtLeastTwo] :
    derivative (ofNat(n) : R[X]) = 0 :=
  derivative_natCast
Derivative of Constant Polynomial $n \geq 2$ is Zero
Informal description
For any natural number $n \geq 2$, the formal derivative of the constant polynomial $n$ in the polynomial ring $R[X]$ is the zero polynomial, i.e., $\frac{d}{dX} n = 0$.
Polynomial.iterate_derivative_eq_zero theorem
{p : R[X]} {x : ℕ} (hx : p.natDegree < x) : Polynomial.derivative^[x] p = 0
Full source 
theorem iterate_derivative_eq_zero {p : R[X]} {x : ℕ} (hx : p.natDegree < x) :
    Polynomial.derivativePolynomial.derivative^[x] p = 0 := by
  induction' h : p.natDegree using Nat.strong_induction_on with _ ih generalizing p x
  subst h
  obtain ⟨t, rfl⟩ := Nat.exists_eq_succ_of_ne_zero (pos_of_gt hx).ne'
  rw [Function.iterate_succ_apply]
  by_cases hp : p.natDegree = 0
  · rw [derivative_of_natDegree_zero hp, iterate_derivative_zero]
  have := natDegree_derivative_lt hp
  exact ih _ this (this.trans_le <| Nat.le_of_lt_succ hx) rfl
Vanishing of High-Order Derivatives: $D^x(p) = 0$ when $\text{natDegree}(p) < x$
Informal description
For any polynomial $p \in R[X]$ and natural number $x$, if the natural degree of $p$ is less than $x$, then the $x$-th iterate of the formal derivative operator applied to $p$ yields the zero polynomial, i.e., $D^x(p) = 0$.
Polynomial.iterate_derivative_C theorem
{k} (h : 0 < k) : derivative^[k] (C a : R[X]) = 0
Full source 
@[simp]
theorem iterate_derivative_C {k} (h : 0 < k) : derivativederivative^[k] (C a : R[X]) = 0 :=
  iterate_derivative_eq_zero <| (natDegree_C _).trans_lt h
Vanishing of High-Order Derivatives for Constant Polynomials: $D^k(a) = 0$ when $k > 0$
Informal description
For any natural number $k > 0$ and any element $a$ in a semiring $R$, the $k$-th iterate of the formal derivative operator applied to the constant polynomial $a$ in $R[X]$ yields the zero polynomial, i.e., $D^k(a) = 0$.
Polynomial.iterate_derivative_one theorem
{k} (h : 0 < k) : derivative^[k] (1 : R[X]) = 0
Full source 
@[simp]
theorem iterate_derivative_one {k} (h : 0 < k) : derivativederivative^[k] (1 : R[X]) = 0 :=
  iterate_derivative_C h
Vanishing of High-Order Derivatives for the Unit Polynomial: $D^k(1) = 0$ when $k > 0$
Informal description
For any natural number $k > 0$, the $k$-th iterate of the formal derivative operator applied to the constant polynomial $1$ in $R[X]$ yields the zero polynomial, i.e., $D^k(1) = 0$.
Polynomial.iterate_derivative_X theorem
{k} (h : 1 < k) : derivative^[k] (X : R[X]) = 0
Full source 
@[simp]
theorem iterate_derivative_X {k} (h : 1 < k) : derivativederivative^[k] (X : R[X]) = 0 :=
  iterate_derivative_eq_zero <| natDegree_X_le.trans_lt h
Vanishing of High-Order Derivatives of $X$: $D^k(X) = 0$ for $k > 1$
Informal description
For any natural number $k > 1$, the $k$-th iterate of the formal derivative operator applied to the polynomial variable $X$ yields the zero polynomial, i.e., $D^k(X) = 0$.
Polynomial.natDegree_eq_zero_of_derivative_eq_zero theorem
[NoZeroSMulDivisors ℕ R] {f : R[X]} (h : derivative f = 0) : f.natDegree = 0
Full source 
theorem natDegree_eq_zero_of_derivative_eq_zero [NoZeroSMulDivisors ℕ R] {f : R[X]}
    (h : derivative f = 0) : f.natDegree = 0 := by
  rcases eq_or_ne f 0 with (rfl | hf)
  · exact natDegree_zero
  rw [natDegree_eq_zero_iff_degree_le_zero]
  by_contra! f_nat_degree_pos
  rw [← natDegree_pos_iff_degree_pos] at f_nat_degree_pos
  let m := f.natDegree - 1
  have hm : m + 1 = f.natDegree := tsub_add_cancel_of_le f_nat_degree_pos
  have h2 := coeff_derivative f m
  rw [Polynomial.ext_iff] at h
  rw [h m, coeff_zero, ← Nat.cast_add_one, ← nsmul_eq_mul', eq_comm, smul_eq_zero] at h2
  replace h2 := h2.resolve_left m.succ_ne_zero
  rw [hm, ← leadingCoeff, leadingCoeff_eq_zero] at h2
  exact hf h2
Constant Polynomials are the Only Polynomials with Zero Derivative in Semirings without Zero Scalar Divisors
Informal description
Let $R$ be a semiring with no zero scalar divisors (i.e., for any $n \in \mathbb{N}$ and $r \in R$, $n \cdot r = 0$ implies $n = 0$ or $r = 0$). For any polynomial $f \in R[X]$, if the formal derivative of $f$ is zero, then the natural degree of $f$ is zero (i.e., $f$ is a constant polynomial).
Polynomial.derivative_mul theorem
{f g : R[X]} : derivative (f * g) = derivative f * g + f * derivative g
Full source 
@[simp]
theorem derivative_mul {f g : R[X]} : derivative (f * g) = derivative f * g + f * derivative g := by
  induction f using Polynomial.induction_on' with
  | add => simp only [add_mul, map_add, add_assoc, add_left_comm, *]
  | monomial m a => ?_
  induction g using Polynomial.induction_on' with
  | add => simp only [mul_add, map_add, add_assoc, add_left_comm, *]
  | monomial n b => ?_
  simp only [monomial_mul_monomial, derivative_monomial]
  simp only [mul_assoc, (Nat.cast_commute _ _).eq, Nat.cast_add, mul_add, map_add]
  cases m with
  | zero => simp only [zero_add, Nat.cast_zero, mul_zero, map_zero]
  | succ m =>
  cases n with
  | zero => simp only [add_zero, Nat.cast_zero, mul_zero, map_zero]
  | succ n =>
  simp only [Nat.add_succ_sub_one, add_tsub_cancel_right]
  rw [add_assoc, add_comm n 1]
Leibniz Rule for Polynomial Derivatives: $\frac{d}{dX}(f \cdot g) = f' \cdot g + f \cdot g'$
Informal description
For any two polynomials $f$ and $g$ in the polynomial ring $R[X]$ over a semiring $R$, the derivative of their product is given by the Leibniz rule: \[ \frac{d}{dX}(f \cdot g) = \frac{df}{dX} \cdot g + f \cdot \frac{dg}{dX}. \]
Polynomial.derivative_eval theorem
(p : R[X]) (x : R) : p.derivative.eval x = p.sum fun n a => a * n * x ^ (n - 1)
Full source 
theorem derivative_eval (p : R[X]) (x : R) :
    p.derivative.eval x = p.sum fun n a => a * n * x ^ (n - 1) := by
  simp_rw [derivative_apply, eval_sum, eval_mul_X_pow, eval_C]
Evaluation of Polynomial Derivative as Sum of Scaled Monomials
Informal description
For any polynomial $p \in R[X]$ over a semiring $R$ and any element $x \in R$, the evaluation of the derivative $p'$ at $x$ is equal to the sum $\sum_{n} (a_n \cdot n \cdot x^{n-1})$, where $p = \sum_n a_n X^n$ is the expansion of $p$.
Polynomial.derivative_map theorem
[Semiring S] (p : R[X]) (f : R →+* S) : derivative (p.map f) = p.derivative.map f
Full source 
@[simp]
theorem derivative_map [Semiring S] (p : R[X]) (f : R →+* S) :
    derivative (p.map f) = p.derivative.map f := by
  let n := max p.natDegree (map f p).natDegree
  rw [derivative_apply, derivative_apply]
  rw [sum_over_range' _ _ (n + 1) ((le_max_left _ _).trans_lt (lt_add_one _))]
  on_goal 1 => rw [sum_over_range' _ _ (n + 1) ((le_max_right _ _).trans_lt (lt_add_one _))]
  · simp only [Polynomial.map_sum, Polynomial.map_mul, Polynomial.map_C, map_mul, coeff_map,
      map_natCast, Polynomial.map_natCast, Polynomial.map_pow, map_X]
  all_goals intro n; rw [zero_mul, C_0, zero_mul]
Derivative Commutes with Polynomial Map under Ring Homomorphism
Informal description
Let $R$ and $S$ be semirings, $p \in R[X]$ a polynomial, and $f \colon R \to S$ a ring homomorphism. Then the derivative of the polynomial $p$ mapped by $f$ equals the derivative of $p$ mapped by $f$, i.e., \[ \frac{d}{dX}(f_* p) = f_*\left(\frac{dp}{dX}\right) \] where $f_*$ denotes the polynomial map induced by $f$.
Polynomial.iterate_derivative_map theorem
[Semiring S] (p : R[X]) (f : R →+* S) (k : ℕ) : Polynomial.derivative^[k] (p.map f) = (Polynomial.derivative^[k] p).map f
Full source 
@[simp]
theorem iterate_derivative_map [Semiring S] (p : R[X]) (f : R →+* S) (k : ℕ) :
    Polynomial.derivativePolynomial.derivative^[k] (p.map f) = (Polynomial.derivativePolynomial.derivative^[k] p).map f := by
  induction' k with k ih generalizing p
  · simp
  · simp only [ih, Function.iterate_succ, Polynomial.derivative_map, Function.comp_apply]
Iterated Derivative Commutes with Polynomial Map under Ring Homomorphism
Informal description
Let $R$ and $S$ be semirings, $p \in R[X]$ a polynomial, $f \colon R \to S$ a ring homomorphism, and $k$ a natural number. Then the $k$-th iterate of the derivative of the polynomial $p$ mapped by $f$ equals the $k$-th iterate of the derivative of $p$ mapped by $f$, i.e., \[ \left(\frac{d}{dX}\right)^k (f_* p) = f_* \left(\left(\frac{d}{dX}\right)^k p\right) \] where $f_*$ denotes the polynomial map induced by $f$ and $\left(\frac{d}{dX}\right)^k$ denotes the $k$-th derivative.
Polynomial.derivative_natCast_mul theorem
{n : ℕ} {f : R[X]} : derivative ((n : R[X]) * f) = n * derivative f
Full source 
theorem derivative_natCast_mul {n : ℕ} {f : R[X]} :
    derivative ((n : R[X]) * f) = n * derivative f := by
  simp
Derivative of Scalar Multiple by Natural Number: $\frac{d}{dX}(n \cdot f) = n \cdot \frac{df}{dX}$
Informal description
For any natural number $n$ and polynomial $f \in R[X]$, the derivative of the product of the constant polynomial $n$ and $f$ is equal to $n$ times the derivative of $f$, i.e., \[ \frac{d}{dX}(n \cdot f) = n \cdot \frac{df}{dX}. \]
Polynomial.iterate_derivative_natCast_mul theorem
{n k : ℕ} {f : R[X]} : derivative^[k] ((n : R[X]) * f) = n * derivative^[k] f
Full source 
@[simp]
theorem iterate_derivative_natCast_mul {n k : ℕ} {f : R[X]} :
    derivativederivative^[k] ((n : R[X]) * f) = n * derivativederivative^[k] f := by
  induction' k with k ih generalizing f <;> simp [*]
Iterated Derivative of Scalar Multiple by Natural Number: $\left(\frac{d}{dX}\right)^k (n \cdot f) = n \cdot \left(\frac{d}{dX}\right)^k f$
Informal description
For any natural numbers $n$ and $k$, and any polynomial $f \in R[X]$, the $k$-th iterate of the derivative of the product of the constant polynomial $n$ and $f$ is equal to $n$ times the $k$-th iterate of the derivative of $f$, i.e., \[ \left(\frac{d}{dX}\right)^k (n \cdot f) = n \cdot \left(\frac{d}{dX}\right)^k f. \]
Polynomial.mem_support_derivative theorem
[NoZeroSMulDivisors ℕ R] (p : R[X]) (n : ℕ) : n ∈ (derivative p).support ↔ n + 1 ∈ p.support
Full source 
theorem mem_support_derivative [NoZeroSMulDivisors ℕ R] (p : R[X]) (n : ℕ) :
    n ∈ (derivative p).supportn ∈ (derivative p).support ↔ n + 1 ∈ p.support := by
  suffices ¬p.coeff (n + 1) * (n + 1 : ℕ) = 0¬p.coeff (n + 1) * (n + 1 : ℕ) = 0 ↔ coeff p (n + 1) ≠ 0 by
    simpa only [mem_support_iff, coeff_derivative, Ne, Nat.cast_succ]
  rw [← nsmul_eq_mul', smul_eq_zero]
  simp only [Nat.succ_ne_zero, false_or]
Support Characterization of Polynomial Derivative: $n \in \text{supp}(p') \leftrightarrow n+1 \in \text{supp}(p)$
Informal description
Let $R$ be a semiring with no zero scalar divisors by $\mathbb{N}$. For any polynomial $p \in R[X]$ and natural number $n$, the exponent $n$ appears in the support of the derivative $p'$ if and only if the exponent $n+1$ appears in the support of $p$. In other words, $X^n$ has a nonzero coefficient in $p'$ if and only if $X^{n+1}$ has a nonzero coefficient in $p$.
Polynomial.degree_derivative_eq theorem
[NoZeroSMulDivisors ℕ R] (p : R[X]) (hp : 0 < natDegree p) : degree (derivative p) = (natDegree p - 1 : ℕ)
Full source 
@[simp]
theorem degree_derivative_eq [NoZeroSMulDivisors ℕ R] (p : R[X]) (hp : 0 < natDegree p) :
    degree (derivative p) = (natDegree p - 1 : ℕ) := by
  apply le_antisymm
  · rw [derivative_apply]
    apply le_trans (degree_sum_le _ _) (Finset.sup_le _)
    intro n hn
    apply le_trans (degree_C_mul_X_pow_le _ _) (WithBot.coe_le_coe.2 (tsub_le_tsub_right _ _))
    apply le_natDegree_of_mem_supp _ hn
  · refine le_sup ?_
    rw [mem_support_derivative, tsub_add_cancel_of_le, mem_support_iff]
    · rw [coeff_natDegree, Ne, leadingCoeff_eq_zero]
      intro h
      rw [h, natDegree_zero] at hp
      exact hp.false
    exact hp
Degree of Polynomial Derivative: $\deg(p') = \deg(p) - 1$ for $\deg(p) > 0$
Informal description
Let $R$ be a semiring with no zero scalar divisors by $\mathbb{N}$. For any polynomial $p \in R[X]$ with positive degree $n > 0$, the degree of its formal derivative $p'$ is equal to $n - 1$.
Polynomial.coeff_iterate_derivative theorem
{k} (p : R[X]) (m : ℕ) : (derivative^[k] p).coeff m = (m + k).descFactorial k • p.coeff (m + k)
Full source 
theorem coeff_iterate_derivative {k} (p : R[X]) (m : ℕ) :
    (derivativederivative^[k] p).coeff m = (m + k).descFactorial k • p.coeff (m + k) := by
  induction k generalizing m with
  | zero => simp
  | succ k ih =>
      calc
        (derivative^[k + 1] p).coeff m
        _ = Nat.descFactorial (Nat.succ (m + k)) k • p.coeff (m + k.succ) * (m + 1) := by
          rw [Function.iterate_succ_apply', coeff_derivative, ih m.succ, Nat.succ_add, Nat.add_succ]
        _ = ((m + 1) * Nat.descFactorial (Nat.succ (m + k)) k) • p.coeff (m + k.succ) := by
          rw [← Nat.cast_add_one, ← nsmul_eq_mul', smul_smul]
        _ = Nat.descFactorial (m.succ + k) k.succ • p.coeff (m + k.succ) := by
          rw [← Nat.succ_add, Nat.descFactorial_succ, add_tsub_cancel_right]
        _ = Nat.descFactorial (m + k.succ) k.succ • p.coeff (m + k.succ) := by
          rw [Nat.succ_add_eq_add_succ]
Coefficient Formula for Iterated Derivative: $\text{coeff}(D^k(p), m) = (m+k)^{\underline{k}} \cdot \text{coeff}(p, m+k)$
Informal description
For any polynomial $p \in R[X]$, natural numbers $k$ and $m$, the coefficient of $X^m$ in the $k$-th iterate of the formal derivative of $p$ is equal to the descending factorial $(m+k)^{\underline{k}}$ multiplied by the coefficient of $X^{m+k}$ in $p$. That is: $$ \text{coeff}(D^k(p), m) = (m+k)^{\underline{k}} \cdot \text{coeff}(p, m+k) $$ where $D^k$ denotes the $k$-th iterate of the formal derivative and $(m+k)^{\underline{k}} = (m+k)(m+k-1)\cdots(m+1)$ is the descending factorial.
Polynomial.iterate_derivative_eq_sum theorem
(p : R[X]) (k : ℕ) : derivative^[k] p = ∑ x ∈ (derivative^[k] p).support, C ((x + k).descFactorial k • p.coeff (x + k)) * X ^ x
Full source 
theorem iterate_derivative_eq_sum (p : R[X]) (k : ℕ) :
    derivativederivative^[k] p =
      ∑ x ∈ (derivative^[k] p).support, C ((x + k).descFactorial k • p.coeff (x + k)) * X ^ x := by
  conv_lhs => rw [(derivativederivative^[k] p).as_sum_support_C_mul_X_pow]
  refine sum_congr rfl fun i _ ↦ ?_
  rw [coeff_iterate_derivative, Nat.descFactorial_eq_factorial_mul_choose]
Sum Formula for Iterated Derivative of Polynomial: $D^k(p) = \sum_{x} C\big((x+k)^{\underline{k}} \cdot a_{x+k}\big) X^x$
Informal description
For any polynomial $p \in R[X]$ and natural number $k$, the $k$-th iterate of the formal derivative of $p$ can be expressed as the sum over its support: $$ D^k(p) = \sum_{x \in \text{supp}(D^k(p))} C\big((x+k)^{\underline{k}} \cdot a_{x+k}\big) \cdot X^x $$ where: - $D^k$ denotes the $k$-th iterate of the formal derivative, - $\text{supp}(D^k(p))$ is the finite set of exponents with nonzero coefficients in $D^k(p)$, - $(x+k)^{\underline{k}} = (x+k)(x+k-1)\cdots(x+1)$ is the descending factorial, - $a_{x+k}$ is the coefficient of $X^{x+k}$ in $p$, - $C$ is the constant polynomial embedding, - $X^x$ is the monomial $X$ raised to the power $x$.
Polynomial.iterate_derivative_eq_factorial_smul_sum theorem
(p : R[X]) (k : ℕ) : derivative^[k] p = k ! • ∑ x ∈ (derivative^[k] p).support, C ((x + k).choose k • p.coeff (x + k)) * X ^ x
Full source 
theorem iterate_derivative_eq_factorial_smul_sum (p : R[X]) (k : ℕ) :
    derivativederivative^[k] p = k ! •
      ∑ x ∈ (derivative^[k] p).support, C ((x + k).choose k • p.coeff (x + k)) * X ^ x := by
  conv_lhs => rw [iterate_derivative_eq_sum]
  rw [smul_sum]
  refine sum_congr rfl fun i _ ↦ ?_
  rw [← smul_mul_assoc, smul_C, smul_smul, Nat.descFactorial_eq_factorial_mul_choose]
Factorial Scaled Sum Formula for Iterated Derivative: $D^k(p) = k! \cdot \sum_{x} C\left(\binom{x+k}{k} \cdot a_{x+k}\right) X^x$
Informal description
For any polynomial $p \in R[X]$ and natural number $k$, the $k$-th iterate of the formal derivative of $p$ can be expressed as: $$ D^k(p) = k! \cdot \sum_{x \in \text{supp}(D^k(p))} C\left(\binom{x+k}{k} \cdot a_{x+k}\right) \cdot X^x $$ where: - $D^k$ denotes the $k$-th iterate of the formal derivative, - $\text{supp}(D^k(p))$ is the finite set of exponents with nonzero coefficients in $D^k(p)$, - $\binom{x+k}{k}$ is the binomial coefficient, - $a_{x+k}$ is the coefficient of $X^{x+k}$ in $p$, - $C$ is the constant polynomial embedding, - $X^x$ is the monomial $X$ raised to the power $x$.
Polynomial.iterate_derivative_mul theorem
{n} (p q : R[X]) : derivative^[n] (p * q) = ∑ k ∈ range n.succ, (n.choose k • (derivative^[n - k] p * derivative^[k] q))
Full source 
theorem iterate_derivative_mul {n} (p q : R[X]) :
    derivativederivative^[n] (p * q) =
      ∑ k ∈ range n.succ, (n.choose k • (derivative^[n - k] p * derivative^[k] q)) := by
  induction n with
  | zero =>
    simp [Finset.range]
  | succ n IH =>
    calc
      derivativederivative^[n + 1] (p * q) =
          derivative (∑ k ∈ range n.succ,
              n.choose k • (derivative^[n - k] p * derivative^[k] q)) := by
        rw [Function.iterate_succ_apply', IH]
      _ = (∑ k ∈ range n.succ,
            n.choose k • (derivative^[n - k + 1] p * derivative^[k] q)) +
          ∑ k ∈ range n.succ,
            n.choose k • (derivative^[n - k] p * derivative^[k + 1] q) := by
        simp_rw [derivative_sum, derivative_smul, derivative_mul, Function.iterate_succ_apply',
          smul_add, sum_add_distrib]
      _ = (∑ k ∈ range n.succ,
                n.choose k.succ • (derivative^[n - k] p * derivative^[k + 1] q)) +
              1 • (derivativederivative^[n + 1] p * derivativederivative^[0] q) +
            ∑ k ∈ range n.succ, n.choose k • (derivative^[n - k] p * derivative^[k + 1] q) :=
        ?_
      _ = ((∑ k ∈ range n.succ, n.choose k • (derivative^[n - k] p * derivative^[k + 1] q)) +
              ∑ k ∈ range n.succ,
                n.choose k.succ • (derivative^[n - k] p * derivative^[k + 1] q)) +
            1 • (derivativederivative^[n + 1] p * derivativederivative^[0] q) := by
        rw [add_comm, add_assoc]
      _ = (∑ i ∈ range n.succ,
              (n + 1).choose (i + 1) • (derivative^[n + 1 - (i + 1)] p * derivative^[i + 1] q)) +
            1 • (derivativederivative^[n + 1] p * derivativederivative^[0] q) := by
        simp_rw [Nat.choose_succ_succ, Nat.succ_sub_succ, add_smul, sum_add_distrib]
      _ = ∑ k ∈ range n.succ.succ,
            n.succ.choose k • (derivative^[n.succ - k] p * derivative^[k] q) := by
        rw [sum_range_succ' _ n.succ, Nat.choose_zero_right, tsub_zero]
    congr
    refine (sum_range_succ' _ _).trans (congr_arg₂ (· + ·) ?_ ?_)
    · rw [sum_range_succ, Nat.choose_succ_self, zero_smul, add_zero]
      refine sum_congr rfl fun k hk => ?_
      rw [mem_range] at hk
      congr
      omega
    · rw [Nat.choose_zero_right, tsub_zero]
Generalized Leibniz Rule for Polynomial Derivatives: $D^n(p \cdot q) = \sum_{k=0}^n \binom{n}{k} D^{n-k}(p) \cdot D^k(q)$
Informal description
For any natural number $n$ and any polynomials $p, q \in R[X]$, the $n$-th iterate of the formal derivative of the product $p \cdot q$ is given by: \[ D^n(p \cdot q) = \sum_{k=0}^n \binom{n}{k} \cdot \left( D^{n-k}(p) \cdot D^k(q) \right), \] where $D^m$ denotes the $m$-th iterate of the formal derivative.
Polynomial.derivativeFinsupp definition
: R[X] →ₗ[R] ℕ →₀ R[X]
Full source 
/--
Iterated derivatives as a finite support function.
-/
@[simps! apply_toFun]
noncomputable def derivativeFinsupp : R[X]R[X] →ₗ[R] ℕ →₀ R[X] where
  toFun p := .onFinset (range (p.natDegree + 1)) (derivativederivative^[·] p) fun i ↦ by
    contrapose; simp_all [iterate_derivative_eq_zero, Nat.succ_le]
  map_add' _ _ := by ext; simp
  map_smul' _ _ := by ext; simp
Iterated derivatives as a finitely supported function
Informal description
The function maps a polynomial \( p \in R[X] \) to a finitely supported function \( \mathbb{N} \to R[X] \) where the support is contained in the range \( \{0, \ldots, \text{natDegree}(p)\} \), and the value at \( n \) is the \( n \)-th formal derivative of \( p \). This is a linear map with respect to the semiring \( R \).
Polynomial.support_derivativeFinsupp_subset_range theorem
{p : R[X]} {n : ℕ} (h : p.natDegree < n) : (derivativeFinsupp p).support ⊆ range n
Full source 
@[simp]
theorem support_derivativeFinsupp_subset_range {p : R[X]} {n : ℕ} (h : p.natDegree < n) :
    (derivativeFinsupp p).support ⊆ range n := by
  dsimp [derivativeFinsupp]
  exact Finsupp.support_onFinset_subset.trans (Finset.range_subset.mpr h)
Support of Iterated Derivatives is Bounded by Degree
Informal description
For any polynomial $p \in R[X]$ and natural number $n$ such that the degree of $p$ is less than $n$, the support of the finitely supported function of iterated derivatives of $p$ is contained in the set $\{0, 1, \ldots, n-1\}$.
Polynomial.derivativeFinsupp_C theorem
(r : R) : derivativeFinsupp (C r : R[X]) = .single 0 (C r)
Full source 
@[simp]
theorem derivativeFinsupp_C (r : R) : derivativeFinsupp (C r : R[X]) = .single 0 (C r) := by
  ext i : 1
  match i with
  | 0 => simp
  | i + 1 => simp
Iterated Derivatives of Constant Polynomials: $D^k(C(r)) = \delta_{k0} C(r)$
Informal description
For any element $r$ in a semiring $R$, the finitely supported function of iterated derivatives of the constant polynomial $C(r) \in R[X]$ is equal to the finitely supported function that takes the value $C(r)$ at $0$ and is zero elsewhere.
Polynomial.derivativeFinsupp_one theorem
: derivativeFinsupp (1 : R[X]) = .single 0 1
Full source 
@[simp]
theorem derivativeFinsupp_one : derivativeFinsupp (1 : R[X]) = .single 0 1 := by
  simpa using derivativeFinsupp_C (1 : R)
Iterated Derivatives of the Constant Polynomial One: $D^k(1) = \delta_{k0} \cdot 1$
Informal description
For the constant polynomial $1 \in R[X]$, the finitely supported function representing its iterated derivatives is equal to the function that takes the value $1$ at $0$ and is zero elsewhere. In other words, the $k$-th derivative of $1$ is $1$ when $k = 0$ and $0$ otherwise.
Polynomial.derivativeFinsupp_X theorem
: derivativeFinsupp (X : R[X]) = .single 0 X + .single 1 1
Full source 
@[simp]
theorem derivativeFinsupp_X : derivativeFinsupp (X : R[X]) = .single 0 X + .single 1 1 := by
  ext i : 1
  match i with
  | 0 => simp
  | 1 => simp
  | (n + 2) => simp
Iterated Derivatives of the Polynomial Variable: $\text{derivativeFinsupp}(X) = \{0 \mapsto X, 1 \mapsto 1\}$
Informal description
For the polynomial variable $X \in R[X]$, the finitely supported function representing its iterated derivatives is given by: \[ \text{derivativeFinsupp}(X) = \text{single}(0, X) + \text{single}(1, 1) \] where: - $\text{single}(0, X)$ represents the 0-th derivative (the polynomial itself) - $\text{single}(1, 1)$ represents the first derivative (the constant polynomial 1)
Polynomial.derivativeFinsupp_map theorem
[Semiring S] (p : R[X]) (f : R →+* S) : derivativeFinsupp (p.map f) = (derivativeFinsupp p).mapRange (·.map f) (by simp)
Full source 
theorem derivativeFinsupp_map [Semiring S] (p : R[X]) (f : R →+* S) :
    derivativeFinsupp (p.map f) = (derivativeFinsupp p).mapRange (·.map f) (by simp) := by
  ext i : 1
  simp
Compatibility of Iterated Derivatives with Polynomial Map under Ring Homomorphism
Informal description
Let $R$ and $S$ be semirings, $p \in R[X]$ a polynomial, and $f \colon R \to S$ a ring homomorphism. Then the finitely supported function representing the iterated derivatives of the polynomial $p$ mapped by $f$ equals the finitely supported function obtained by applying $f$ to each coefficient of the iterated derivatives of $p$. In other words, if we denote $D^{(n)}(p)$ as the $n$-th derivative of $p$, then: \[ \text{derivativeFinsupp}(f_* p) = \text{mapRange}(f_*, \text{derivativeFinsupp}(p)) \] where $f_*$ denotes the polynomial map induced by $f$.
Polynomial.derivativeFinsupp_derivative theorem
(p : R[X]) : derivativeFinsupp (derivative p) = (derivativeFinsupp p).comapDomain Nat.succ Nat.succ_injective.injOn
Full source 
theorem derivativeFinsupp_derivative (p : R[X]) :
    derivativeFinsupp (derivative p) =
      (derivativeFinsupp p).comapDomain Nat.succ Nat.succ_injective.injOn := by
  ext i : 1
  simp
Iterated Derivatives of Polynomial Derivative via Successor Preimage
Informal description
For any polynomial $p \in R[X]$, the finitely supported function representing the iterated derivatives of the derivative of $p$ is equal to the preimage composition of the finitely supported function representing the iterated derivatives of $p$ under the successor function $\mathrm{succ} \colon \mathbb{N} \to \mathbb{N}$. More precisely, if we denote $D^{(n)}(p)$ as the $n$-th derivative of $p$, then: \[ \text{derivativeFinsupp}(D(p)) = \text{comapDomain}(\mathrm{succ}, \text{derivativeFinsupp}(p)) \] where $\mathrm{succ}$ is injective on the support of $\text{derivativeFinsupp}(p)$.
Polynomial.derivative_pow_succ theorem
(p : R[X]) (n : ℕ) : derivative (p ^ (n + 1)) = C (n + 1 : R) * p ^ n * derivative p
Full source 
theorem derivative_pow_succ (p : R[X]) (n : ℕ) :
    derivative (p ^ (n + 1)) = C (n + 1 : R) * p ^ n * derivative p :=
  Nat.recOn n (by simp) fun n ih => by
    rw [pow_succ, derivative_mul, ih, Nat.add_one, mul_right_comm, C_add,
      add_mul, add_mul, pow_succ, ← mul_assoc, C_1, one_mul]; simp [add_mul]
Derivative of Polynomial Power: $\frac{d}{dX}(p^{n+1}) = (n+1) p^n p'$
Informal description
For any polynomial $p \in R[X]$ over a semiring $R$ and any natural number $n$, the derivative of $p^{n+1}$ is given by: \[ \frac{d}{dX}(p^{n+1}) = (n+1) \cdot p^n \cdot \frac{dp}{dX} \] where $(n+1)$ is interpreted as a constant polynomial via the embedding $C \colon R \to R[X]$.
Polynomial.derivative_pow theorem
(p : R[X]) (n : ℕ) : derivative (p ^ n) = C (n : R) * p ^ (n - 1) * derivative p
Full source 
theorem derivative_pow (p : R[X]) (n : ℕ) :
    derivative (p ^ n) = C (n : R) * p ^ (n - 1) * derivative p :=
  Nat.casesOn n (by rw [pow_zero, derivative_one, Nat.cast_zero, C_0, zero_mul, zero_mul]) fun n =>
    by rw [p.derivative_pow_succ n, Nat.add_one_sub_one, n.cast_succ]
Power Rule for Polynomial Derivatives: $\frac{d}{dX}(p^n) = n p^{n-1} p'$
Informal description
For any polynomial $p \in R[X]$ over a commutative semiring $R$ and any natural number $n$, the derivative of $p^n$ is given by: \[ \frac{d}{dX}(p^n) = n \cdot p^{n-1} \cdot \frac{dp}{dX} \] where $n$ is interpreted as a constant polynomial via the embedding $C \colon R \to R[X]$.
Polynomial.derivative_sq theorem
(p : R[X]) : derivative (p ^ 2) = C 2 * p * derivative p
Full source 
theorem derivative_sq (p : R[X]) : derivative (p ^ 2) = C 2 * p * derivative p := by
  rw [derivative_pow_succ, Nat.cast_one, one_add_one_eq_two, pow_one]
Derivative of Squared Polynomial: $\frac{d}{dX}(p^2) = 2 p p'$
Informal description
For any polynomial $p$ over a semiring $R$, the derivative of $p^2$ is given by: \[ \frac{d}{dX}(p^2) = 2 \cdot p \cdot \frac{dp}{dX} \] where $2$ is interpreted as a constant polynomial via the embedding $C \colon R \to R[X]$.
Polynomial.pow_sub_one_dvd_derivative_of_pow_dvd theorem
{p q : R[X]} {n : ℕ} (dvd : q ^ n ∣ p) : q ^ (n - 1) ∣ derivative p
Full source 
theorem pow_sub_one_dvd_derivative_of_pow_dvd {p q : R[X]} {n : ℕ}
    (dvd : q ^ n ∣ p) : q ^ (n - 1) ∣ derivative p := by
  obtain ⟨r, rfl⟩ := dvd
  rw [derivative_mul, derivative_pow]
  exact (((dvd_mul_left _ _).mul_right _).mul_right _).add ((pow_dvd_pow q n.pred_le).mul_right _)
Divisibility of Derivative by Reduced Power: $q^n \mid p \Rightarrow q^{n-1} \mid p'$
Informal description
For any polynomials $p, q \in R[X]$ over a commutative semiring $R$ and any natural number $n$, if $q^n$ divides $p$, then $q^{n-1}$ divides the derivative of $p$.
Polynomial.pow_sub_dvd_iterate_derivative_of_pow_dvd theorem
{p q : R[X]} {n : ℕ} (m : ℕ) (dvd : q ^ n ∣ p) : q ^ (n - m) ∣ derivative^[m] p
Full source 
theorem pow_sub_dvd_iterate_derivative_of_pow_dvd {p q : R[X]} {n : ℕ} (m : ℕ)
    (dvd : q ^ n ∣ p) : q ^ (n - m) ∣ derivative^[m] p := by
  induction m generalizing p with
  | zero => simpa
  | succ m ih =>
    rw [Nat.sub_succ, Function.iterate_succ']
    exact pow_sub_one_dvd_derivative_of_pow_dvd (ih dvd)
Divisibility of Iterated Derivative by Reduced Power: $q^n \mid p \Rightarrow q^{n-m} \mid p^{(m)}$
Informal description
For any polynomials $p, q \in R[X]$ over a commutative semiring $R$ and natural numbers $n, m$, if $q^n$ divides $p$, then $q^{n-m}$ divides the $m$-th iterate of the derivative of $p$.
Polynomial.pow_sub_dvd_iterate_derivative_pow theorem
(p : R[X]) (n m : ℕ) : p ^ (n - m) ∣ derivative^[m] (p ^ n)
Full source 
theorem pow_sub_dvd_iterate_derivative_pow (p : R[X]) (n m : ℕ) :
    p ^ (n - m) ∣ derivative^[m] (p ^ n) := pow_sub_dvd_iterate_derivative_of_pow_dvd m dvd_rfl
Divisibility of Iterated Derivative of Power: $p^{n-m} \mid (p^n)^{(m)}$
Informal description
For any polynomial $p \in R[X]$ over a commutative semiring $R$ and natural numbers $n, m$, the $(n-m)$-th power of $p$ divides the $m$-th iterate of the derivative of $p^n$. That is, \[ p^{n-m} \mid \left(\frac{d}{dX}\right)^m (p^n). \]
Polynomial.dvd_iterate_derivative_pow theorem
(f : R[X]) (n : ℕ) {m : ℕ} (c : R) (hm : m ≠ 0) : (n : R) ∣ eval c (derivative^[m] (f ^ n))
Full source 
theorem dvd_iterate_derivative_pow (f : R[X]) (n : ℕ) {m : ℕ} (c : R) (hm : m ≠ 0) :
    (n : R) ∣ eval c (derivative^[m] (f ^ n)) := by
  obtain ⟨m, rfl⟩ := Nat.exists_eq_succ_of_ne_zero hm
  rw [Function.iterate_succ_apply, derivative_pow, mul_assoc, C_eq_natCast,
    iterate_derivative_natCast_mul, eval_mul, eval_natCast]
  exact dvd_mul_right _ _
Divisibility of Evaluated Iterated Derivative of Polynomial Power: $n \mid \left(\frac{d}{dX}\right)^m (f^n)(c)$
Informal description
Let $R$ be a commutative semiring and $f \in R[X]$ be a polynomial. For any natural numbers $n$ and $m \neq 0$, and any element $c \in R$, the evaluation of the $m$-th iterate of the derivative of $f^n$ at $c$ is divisible by $n$ in $R$. That is, \[ n \mid \left(\frac{d}{dX}\right)^m (f^n)\big|_{X = c}. \]
Polynomial.iterate_derivative_X_pow_eq_natCast_mul theorem
(n k : ℕ) : derivative^[k] (X ^ n : R[X]) = ↑(Nat.descFactorial n k : R[X]) * X ^ (n - k)
Full source 
theorem iterate_derivative_X_pow_eq_natCast_mul (n k : ℕ) :
    derivativederivative^[k] (X ^ n : R[X]) = ↑(Nat.descFactorial n k : R[X]) * X ^ (n - k) := by
  induction k with
  | zero =>
    rw [Function.iterate_zero_apply, tsub_zero, Nat.descFactorial_zero, Nat.cast_one, one_mul]
  | succ k ih =>
    rw [Function.iterate_succ_apply', ih, derivative_natCast_mul, derivative_X_pow, C_eq_natCast,
      Nat.descFactorial_succ, Nat.sub_sub, Nat.cast_mul]
    simp [mul_comm, mul_assoc, mul_left_comm]
$k$-th Derivative of $X^n$: $\frac{d^k}{dX^k}(X^n) = n^{\underline{k}} X^{n-k}$
Informal description
For any natural numbers $n$ and $k$, the $k$-th iterate of the derivative of the monomial $X^n$ in the polynomial ring $R[X]$ is equal to the product of the descending factorial $n^{\underline{k}}$ (interpreted as a constant polynomial) and $X^{n-k}$. That is, \[ \frac{d^k}{dX^k}(X^n) = n^{\underline{k}} \cdot X^{n-k}. \]
Polynomial.iterate_derivative_X_pow_eq_C_mul theorem
(n k : ℕ) : derivative^[k] (X ^ n : R[X]) = C (Nat.descFactorial n k : R) * X ^ (n - k)
Full source 
theorem iterate_derivative_X_pow_eq_C_mul (n k : ℕ) :
    derivativederivative^[k] (X ^ n : R[X]) = C (Nat.descFactorial n k : R) * X ^ (n - k) := by
  rw [iterate_derivative_X_pow_eq_natCast_mul n k, C_eq_natCast]
$k$-th Derivative of Monomial: $\frac{d^k}{dX^k}(X^n) = n^{\underline{k}} X^{n-k}$
Informal description
For any natural numbers $n$ and $k$, the $k$-th iterate of the derivative of the monomial $X^n$ in the polynomial ring $R[X]$ is equal to the constant polynomial $n^{\underline{k}}$ multiplied by $X^{n-k}$. That is, \[ \frac{d^k}{dX^k}(X^n) = n^{\underline{k}} \cdot X^{n-k}, \] where $n^{\underline{k}} = n(n-1)\cdots(n-k+1)$ is the descending factorial.
Polynomial.iterate_derivative_X_pow_eq_smul theorem
(n : ℕ) (k : ℕ) : derivative^[k] (X ^ n : R[X]) = (Nat.descFactorial n k : R) • X ^ (n - k)
Full source 
theorem iterate_derivative_X_pow_eq_smul (n : ℕ) (k : ℕ) :
    derivativederivative^[k] (X ^ n : R[X]) = (Nat.descFactorial n k : R) • X ^ (n - k) := by
  rw [iterate_derivative_X_pow_eq_C_mul n k, smul_eq_C_mul]
$k$-th Derivative of Monomial via Scalar Multiplication: $\frac{d^k}{dX^k}(X^n) = n^{\underline{k}} \cdot X^{n-k}$
Informal description
For any natural numbers $n$ and $k$, the $k$-th iterate of the derivative of the monomial $X^n$ in the polynomial ring $R[X]$ is equal to the scalar multiplication of the descending factorial $n^{\underline{k}}$ (interpreted as an element of $R$) with $X^{n-k}$. That is, \[ \frac{d^k}{dX^k}(X^n) = n^{\underline{k}} \cdot X^{n-k}, \] where $n^{\underline{k}} = n(n-1)\cdots(n-k+1)$ is the descending factorial.
Polynomial.derivative_X_add_C_pow theorem
(c : R) (m : ℕ) : derivative ((X + C c) ^ m) = C (m : R) * (X + C c) ^ (m - 1)
Full source 
theorem derivative_X_add_C_pow (c : R) (m : ℕ) :
    derivative ((X + C c) ^ m) = C (m : R) * (X + C c) ^ (m - 1) := by
  rw [derivative_pow, derivative_X_add_C, mul_one]
Power Rule for Derivative of $(X + c)^m$: $\frac{d}{dX}((X + c)^m) = m (X + c)^{m-1}$
Informal description
For any element $c$ in a commutative semiring $R$ and any natural number $m$, the derivative of the polynomial $(X + c)^m$ in $R[X]$ is given by: \[ \frac{d}{dX}\left((X + c)^m\right) = m \cdot (X + c)^{m-1}, \] where $m$ is interpreted as a constant polynomial via the embedding $C \colon R \to R[X]$.
Polynomial.derivative_X_add_C_sq theorem
(c : R) : derivative ((X + C c) ^ 2) = C 2 * (X + C c)
Full source 
theorem derivative_X_add_C_sq (c : R) : derivative ((X + C c) ^ 2) = C 2 * (X + C c) := by
  rw [derivative_sq, derivative_X_add_C, mul_one]
Derivative of Squared Linear Polynomial: $\frac{d}{dX}((X + c)^2) = 2(X + c)$
Informal description
For any element $c$ in a semiring $R$, the derivative of the squared polynomial $(X + c)^2$ in $R[X]$ is given by: \[ \frac{d}{dX}\big((X + c)^2\big) = 2 \cdot (X + c) \] where $2$ is interpreted as a constant polynomial via the embedding $C \colon R \to R[X]$.
Polynomial.iterate_derivative_X_add_pow theorem
(n k : ℕ) (c : R) : derivative^[k] ((X + C c) ^ n) = Nat.descFactorial n k • (X + C c) ^ (n - k)
Full source 
theorem iterate_derivative_X_add_pow (n k : ℕ) (c : R) :
    derivativederivative^[k] ((X + C c) ^ n) = Nat.descFactorial n k • (X + C c) ^ (n - k) := by
  induction k with
  | zero => simp
  | succ k IH =>
      rw [Nat.sub_succ', Function.iterate_succ_apply', IH, derivative_smul,
        derivative_X_add_C_pow, map_natCast, Nat.descFactorial_succ, nsmul_eq_mul, nsmul_eq_mul,
        Nat.cast_mul]
      ring
$k$-th Derivative of $(X + c)^n$: $\frac{d^k}{dX^k}((X + c)^n) = n^{\underline{k}}(X + c)^{n-k}$
Informal description
For any natural numbers $n$ and $k$, and any element $c$ in a commutative semiring $R$, the $k$-th derivative of the polynomial $(X + c)^n$ in $R[X]$ is given by: \[ \frac{d^k}{dX^k}\big((X + c)^n\big) = n^{\underline{k}} \cdot (X + c)^{n-k} \] where $n^{\underline{k}} = n(n-1)\cdots(n-k+1)$ is the descending factorial of $n$ and $k$.
Polynomial.derivative_comp theorem
(p q : R[X]) : derivative (p.comp q) = derivative q * p.derivative.comp q
Full source 
theorem derivative_comp (p q : R[X]) :
    derivative (p.comp q) = derivative q * p.derivative.comp q := by
  induction p using Polynomial.induction_on'
  · simp [*, mul_add]
  · simp only [derivative_pow, derivative_mul, monomial_comp, derivative_monomial, derivative_C,
      zero_mul, C_eq_natCast, zero_add, RingHom.map_mul]
    ring
Chain Rule for Polynomial Composition: $\frac{d}{dX}(p \circ q) = q' \cdot (p' \circ q)$
Informal description
For any two polynomials $p, q \in R[X]$ over a commutative semiring $R$, the derivative of the composition $p \circ q$ is given by: \[ \frac{d}{dX}(p \circ q) = q' \cdot (p' \circ q) \] where $p'$ and $q'$ denote the derivatives of $p$ and $q$ respectively, and $\circ$ denotes polynomial composition.
Polynomial.derivative_eval₂_C theorem
(p q : R[X]) : derivative (p.eval₂ C q) = p.derivative.eval₂ C q * derivative q
Full source 
/-- Chain rule for formal derivative of polynomials. -/
theorem derivative_eval₂_C (p q : R[X]) :
    derivative (p.eval₂ C q) = p.derivative.eval₂ C q * derivative q :=
  Polynomial.induction_on p (fun r => by rw [eval₂_C, derivative_C, eval₂_zero, zero_mul])
    (fun p₁ p₂ ih₁ ih₂ => by
      rw [eval₂_add, derivative_add, ih₁, ih₂, derivative_add, eval₂_add, add_mul])
    fun n r ih => by
    rw [pow_succ, ← mul_assoc, eval₂_mul, eval₂_X, derivative_mul, ih, @derivative_mul _ _ _ X,
      derivative_X, mul_one, eval₂_add, @eval₂_mul _ _ _ _ X, eval₂_X, add_mul, mul_right_comm]
Chain Rule for Polynomial Composition: $\frac{d}{dX} p(q) = p'(q) \cdot q'$
Informal description
For any polynomials $p, q \in R[X]$ over a commutative semiring $R$, the derivative of the composition $p(q)$ (evaluated using the constant embedding $C$) is given by: \[ \frac{d}{dX} p(q) = p'(q) \cdot q' \] where $p'$ and $q'$ denote the derivatives of $p$ and $q$ respectively.
Polynomial.derivative_prod theorem
[DecidableEq ι] {s : Multiset ι} {f : ι → R[X]} : derivative (Multiset.map f s).prod = (Multiset.map (fun i => (Multiset.map f (s.erase i)).prod * derivative (f i)) s).sum
Full source 
theorem derivative_prod [DecidableEq ι] {s : Multiset ι} {f : ι → R[X]} :
    derivative (Multiset.map f s).prod =
      (Multiset.map (fun i => (Multiset.map f (s.erase i)).prod * derivative (f i)) s).sum := by
  refine Multiset.induction_on s (by simp) fun i s h => ?_
  rw [Multiset.map_cons, Multiset.prod_cons, derivative_mul, Multiset.map_cons _ i s,
    Multiset.sum_cons, Multiset.erase_cons_head, mul_comm (derivative (f i))]
  congr
  rw [h, ← AddMonoidHom.coe_mulLeft, (AddMonoidHom.mulLeft (f i)).map_multiset_sum _,
    AddMonoidHom.coe_mulLeft]
  simp only [Function.comp_apply, Multiset.map_map]
  refine congr_arg _ (Multiset.map_congr rfl fun j hj => ?_)
  rw [← mul_assoc, ← Multiset.prod_cons, ← Multiset.map_cons]
  by_cases hij : i = j
  · simp [hij, ← Multiset.prod_cons, ← Multiset.map_cons, Multiset.cons_erase hj]
  · simp [hij]
Generalized Leibniz Rule for Polynomial Derivatives: $\frac{d}{dX}\prod f_i = \sum (\prod_{j \neq i} f_j) \cdot f_i'$
Informal description
Let $R$ be a commutative semiring and $\iota$ be a type with decidable equality. For any multiset $s$ over $\iota$ and any function $f \colon \iota \to R[X]$, the derivative of the product of polynomials $\prod_{i \in s} f(i)$ is equal to the sum over $s$ of terms where for each $i \in s$, we take the product of the derivative of $f(i)$ with the product of all $f(j)$ for $j \neq i$ in $s$. More precisely: \[ \frac{d}{dX}\left(\prod_{i \in s} f(i)\right) = \sum_{i \in s} \left( \left(\prod_{\substack{j \in s \\ j \neq i}} f(j)\right) \cdot \frac{df(i)}{dX} \right) \]
Polynomial.derivative_neg theorem
(f : R[X]) : derivative (-f) = -derivative f
Full source 
@[simp]
theorem derivative_neg (f : R[X]) : derivative (-f) = -derivative f :=
  LinearMap.map_neg derivative f
Derivative of Negative Polynomial: $D(-f) = -D(f)$
Informal description
For any polynomial $f \in R[X]$ over a ring $R$, the derivative of $-f$ is equal to the negative of the derivative of $f$, i.e., \[ D(-f) = -D(f) \] where $D$ denotes the formal derivative operator on polynomials.
Polynomial.iterate_derivative_neg theorem
{f : R[X]} {k : ℕ} : derivative^[k] (-f) = -derivative^[k] f
Full source 
theorem iterate_derivative_neg {f : R[X]} {k : ℕ} : derivativederivative^[k] (-f) = -derivativederivative^[k] f :=
  iterate_map_neg derivative k f
Iterated Derivative of Negative Polynomial: $D^k(-f) = -D^k(f)$
Informal description
For any polynomial $f \in R[X]$ and natural number $k$, the $k$-th iterate of the formal derivative applied to $-f$ equals the negation of the $k$-th iterate of the derivative applied to $f$, i.e., \[ D^k(-f) = -D^k(f) \] where $D$ denotes the formal derivative operator on polynomials.
Polynomial.derivative_sub theorem
{f g : R[X]} : derivative (f - g) = derivative f - derivative g
Full source 
@[simp]
theorem derivative_sub {f g : R[X]} : derivative (f - g) = derivative f - derivative g :=
  LinearMap.map_sub derivative f g
Derivative of Polynomial Difference Equals Difference of Derivatives
Informal description
For any polynomials $f, g \in R[X]$ over a ring $R$, the derivative of their difference is equal to the difference of their derivatives, i.e., \[ D(f - g) = D(f) - D(g), \] where $D$ denotes the formal derivative operator on $R[X]$.
Polynomial.derivative_X_sub_C theorem
(c : R) : derivative (X - C c) = 1
Full source 
theorem derivative_X_sub_C (c : R) : derivative (X - C c) = 1 := by
  rw [derivative_sub, derivative_X, derivative_C, sub_zero]
Derivative of Linear Polynomial $X - c$ is 1
Informal description
For any element $c$ in a ring $R$, the formal derivative of the polynomial $X - c$ in $R[X]$ is equal to the constant polynomial $1$, i.e., \[ \frac{d}{dX}(X - c) = 1. \]
Polynomial.iterate_derivative_sub theorem
{k : ℕ} {f g : R[X]} : derivative^[k] (f - g) = derivative^[k] f - derivative^[k] g
Full source 
theorem iterate_derivative_sub {k : ℕ} {f g : R[X]} :
    derivativederivative^[k] (f - g) = derivativederivative^[k] f - derivativederivative^[k] g :=
  iterate_map_sub derivative k f g
Iterated Derivative Preserves Subtraction of Polynomials
Informal description
For any natural number $k$ and polynomials $f, g \in R[X]$, the $k$-th iterate of the derivative operator applied to the difference $f - g$ equals the difference of the $k$-th iterated derivatives of $f$ and $g$, i.e., \[ D^k(f - g) = D^k f - D^k g \] where $D$ denotes the formal derivative operator on $R[X]$.
Polynomial.derivative_intCast theorem
{n : ℤ} : derivative (n : R[X]) = 0
Full source 
@[simp]
theorem derivative_intCast {n : ℤ} : derivative (n : R[X]) = 0 := by
  rw [← C_eq_intCast n]
  exact derivative_C
Derivative of Integer Constant Polynomial is Zero
Informal description
For any integer $n \in \mathbb{Z}$, the formal derivative of the constant polynomial $n$ in the polynomial ring $R[X]$ is the zero polynomial, i.e., $\frac{d}{dX} n = 0$.
Polynomial.derivative_intCast_mul theorem
{n : ℤ} {f : R[X]} : derivative ((n : R[X]) * f) = n * derivative f
Full source 
theorem derivative_intCast_mul {n : ℤ} {f : R[X]} : derivative ((n : R[X]) * f) =
    n * derivative f := by
  simp
Derivative of Integer-Scaled Polynomial: $\frac{d}{dX}(n \cdot f) = n \cdot f'$
Informal description
For any integer $n \in \mathbb{Z}$ and polynomial $f \in R[X]$, the derivative of the product of the constant polynomial $n$ and $f$ satisfies: \[ \frac{d}{dX}(n \cdot f) = n \cdot \frac{df}{dX}. \]
Polynomial.iterate_derivative_intCast_mul theorem
{n : ℤ} {k : ℕ} {f : R[X]} : derivative^[k] ((n : R[X]) * f) = n * derivative^[k] f
Full source 
@[simp]
theorem iterate_derivative_intCast_mul {n : ℤ} {k : ℕ} {f : R[X]} :
    derivativederivative^[k] ((n : R[X]) * f) = n * derivativederivative^[k] f := by
  induction' k with k ih generalizing f <;> simp [*]
Iterated Derivative of Scalar Multiple: $\frac{d^k}{dX^k}(n \cdot f) = n \cdot \frac{d^k}{dX^k} f$
Informal description
For any integer $n \in \mathbb{Z}$, natural number $k \in \mathbb{N}$, and polynomial $f \in R[X]$, the $k$-th iterate of the derivative of the product $(n \cdot f)$ is equal to $n$ multiplied by the $k$-th iterate of the derivative of $f$, i.e., \[ \frac{d^k}{dX^k} (n \cdot f) = n \cdot \frac{d^k}{dX^k} f. \]
Polynomial.derivative_comp_one_sub_X theorem
(p : R[X]) : derivative (p.comp (1 - X)) = -p.derivative.comp (1 - X)
Full source 
theorem derivative_comp_one_sub_X (p : R[X]) :
    derivative (p.comp (1 - X)) = -p.derivative.comp (1 - X) := by simp [derivative_comp]
Derivative of Composition with $(1 - X)$: $\frac{d}{dX} p(1 - X) = -p'(1 - X)$
Informal description
For any polynomial $p \in R[X]$ over a commutative ring $R$, the derivative of the composition $p(1 - X)$ is equal to the negative of the composition of the derivative $p'$ with $(1 - X)$, i.e., \[ \frac{d}{dX} p(1 - X) = -p'(1 - X). \]
Polynomial.iterate_derivative_comp_one_sub_X theorem
(p : R[X]) (k : ℕ) : derivative^[k] (p.comp (1 - X)) = (-1) ^ k * (derivative^[k] p).comp (1 - X)
Full source 
@[simp]
theorem iterate_derivative_comp_one_sub_X (p : R[X]) (k : ℕ) :
    derivativederivative^[k] (p.comp (1 - X)) = (-1) ^ k * (derivativederivative^[k] p).comp (1 - X) := by
  induction' k with k ih generalizing p
  · simp
  · simp [ih (derivative p), iterate_derivative_neg, derivative_comp, pow_succ]
Iterated Derivative of Polynomial Composition with $(1 - X)$: $\frac{d^k}{dX^k} p(1 - X) = (-1)^k \cdot p^{(k)}(1 - X)$
Informal description
For any polynomial $p \in R[X]$ and natural number $k$, the $k$-th iterate of the derivative of the composition $p(1 - X)$ is equal to $(-1)^k$ times the composition of the $k$-th derivative of $p$ with $(1 - X)$, i.e., \[ \frac{d^k}{dX^k} p(1 - X) = (-1)^k \cdot (p^{(k)})(1 - X). \]
Polynomial.eval_multiset_prod_X_sub_C_derivative theorem
[DecidableEq R] {S : Multiset R} {r : R} (hr : r ∈ S) : eval r (derivative (Multiset.map (fun a => X - C a) S).prod) = (Multiset.map (fun a => r - a) (S.erase r)).prod
Full source 
theorem eval_multiset_prod_X_sub_C_derivative [DecidableEq R]
    {S : Multiset R} {r : R} (hr : r ∈ S) :
    eval r (derivative (Multiset.map (fun a => X - C a) S).prod) =
      (Multiset.map (fun a => r - a) (S.erase r)).prod := by
  nth_rw 1 [← Multiset.cons_erase hr]
  have := (evalRingHom r).map_multiset_prod (Multiset.map (fun a => X - C a) (S.erase r))
  simpa using this
Evaluation of the Derivative of $\prod (X - a)$ at $r$ Equals $\prod (r - a)$ over $S \setminus \{r\}$
Informal description
Let $R$ be a commutative ring with decidable equality, $S$ be a multiset of elements in $R$, and $r \in R$ be an element contained in $S$. Then, evaluating the derivative of the product $\prod_{a \in S} (X - a)$ at $X = r$ yields the product $\prod_{a \in S \setminus \{r\}} (r - a)$. In other words, \[ \left.\frac{d}{dX}\left(\prod_{a \in S} (X - a)\right)\right|_{X = r} = \prod_{a \in S \setminus \{r\}} (r - a). \]
Polynomial.derivative_X_sub_C_pow theorem
(c : R) (m : ℕ) : derivative ((X - C c) ^ m) = C (m : R) * (X - C c) ^ (m - 1)
Full source 
theorem derivative_X_sub_C_pow (c : R) (m : ℕ) :
    derivative ((X - C c) ^ m) = C (m : R) * (X - C c) ^ (m - 1) := by
  rw [derivative_pow, derivative_X_sub_C, mul_one]
Derivative of $(X - c)^m$: $\frac{d}{dX} (X - c)^m = m (X - c)^{m-1}$
Informal description
For any element $c$ in a commutative ring $R$ and any natural number $m$, the derivative of the polynomial $(X - c)^m$ is given by: \[ \frac{d}{dX} \left( (X - c)^m \right) = m \cdot (X - c)^{m-1}, \] where $m$ is interpreted as a constant polynomial via the embedding $C \colon R \to R[X]$.
Polynomial.derivative_X_sub_C_sq theorem
(c : R) : derivative ((X - C c) ^ 2) = C 2 * (X - C c)
Full source 
theorem derivative_X_sub_C_sq (c : R) : derivative ((X - C c) ^ 2) = C 2 * (X - C c) := by
  rw [derivative_sq, derivative_X_sub_C, mul_one]
Derivative of Squared Linear Polynomial: $\frac{d}{dX}((X - c)^2) = 2(X - c)$
Informal description
For any element $c$ in a commutative ring $R$, the derivative of the squared polynomial $(X - c)^2$ is given by: \[ \frac{d}{dX}\left((X - c)^2\right) = 2 \cdot (X - c), \] where $2$ is interpreted as a constant polynomial via the embedding $C \colon R \to R[X]$.
Polynomial.iterate_derivative_X_sub_pow theorem
(n k : ℕ) (c : R) : derivative^[k] ((X - C c) ^ n) = n.descFactorial k • (X - C c) ^ (n - k)
Full source 
theorem iterate_derivative_X_sub_pow (n k : ℕ) (c : R) :
    derivativederivative^[k] ((X - C c) ^ n) = n.descFactorial k • (X - C c) ^ (n - k) := by
  rw [sub_eq_add_neg, ← C_neg, iterate_derivative_X_add_pow]
$k$-th Derivative of $(X - c)^n$: $\frac{d^k}{dX^k}((X - c)^n) = n^{\underline{k}}(X - c)^{n-k}$
Informal description
For any natural numbers $n$ and $k$, and any element $c$ in a commutative semiring $R$, the $k$-th derivative of the polynomial $(X - c)^n$ in $R[X]$ is given by: \[ \frac{d^k}{dX^k}\big((X - c)^n\big) = n^{\underline{k}} \cdot (X - c)^{n-k} \] where $n^{\underline{k}} = n(n-1)\cdots(n-k+1)$ is the descending factorial of $n$ and $k$.
Polynomial.iterate_derivative_X_sub_pow_self theorem
(n : ℕ) (c : R) : derivative^[n] ((X - C c) ^ n) = n.factorial
Full source 
theorem iterate_derivative_X_sub_pow_self (n : ℕ) (c : R) :
    derivativederivative^[n] ((X - C c) ^ n) = n.factorial := by
  rw [iterate_derivative_X_sub_pow, n.sub_self, pow_zero, nsmul_one, n.descFactorial_self]
$n$-th Derivative of $(X - c)^n$ is $n!$
Informal description
For any natural number $n$ and any element $c$ in a commutative semiring $R$, the $n$-th derivative of the polynomial $(X - c)^n$ in $R[X]$ is equal to the factorial of $n$, i.e., \[ \frac{d^n}{dX^n}\big((X - c)^n\big) = n! \]
Polynomial.dvd_derivative_iff theorem
{P : R[X]} : P ∣ derivative P ↔ derivative P = 0
Full source 
@[simp]
theorem dvd_derivative_iff {P : R[X]} : P ∣ derivative PP ∣ derivative P ↔ derivative P = 0 where
  mp h := by
    by_cases hP : P = 0
    · simp only [hP, derivative_zero]
    exact eq_zero_of_dvd_of_degree_lt h (degree_derivative_lt hP)
  mpr h := by simp [h]
Divisibility Condition for Polynomial Derivatives: $P \mid P' \Leftrightarrow P' = 0$
Informal description
For any polynomial $P$ over a semiring $R$, $P$ divides its formal derivative $P'$ if and only if $P'$ is the zero polynomial.
Polynomial.derivative_pow_eq_zero theorem
{n : ℕ} (chn : (n : R) ≠ 0) {a : R[X]} : derivative (a ^ n) = 0 ↔ derivative a = 0
Full source 
theorem derivative_pow_eq_zero {n : ℕ} (chn : (n : R) ≠ 0) {a : R[X]} :
    derivativederivative (a ^ n) = 0 ↔ derivative a = 0 := by
  nontriviality R
  rw [← C_ne_zero, C_eq_natCast] at chn
  simp +contextual [derivative_pow, or_imp, chn]
Vanishing Derivative Condition for Powers: $\frac{d}{dX}(a^n) = 0 \leftrightarrow \frac{d}{dX}a = 0$ when $n \neq 0$ in $R$
Informal description
For any natural number $n$ and polynomial $a \in R[X]$ over a commutative semiring $R$, if the natural number $n$ is nonzero in $R$ (i.e., $n \neq 0$ in $R$), then the derivative of $a^n$ is zero if and only if the derivative of $a$ is zero. In other words: \[ \frac{d}{dX}(a^n) = 0 \leftrightarrow \frac{d}{dX}a = 0 \]