derivativeFinsupp_derivative — Mathlib

English

For all n ∈ ℕ and k ∈ ℕ, the k-th iterate of the derivative on X^n equals (n_descFactorial_k)·X^{n−k}, i.e., derivative^[k](X^n) = (n_descFactorial k) · X^{n−k}.

Русский

Для всех n, k ∈ ℕ производная^[k](X^n) = (n_descFactorial k) · X^{n−k}.

LaTeX

$$$$ \operatorname{derivative}^{k}(X^{n}) = (n \downarrow k) \cdot X^{n-k} $$$$

Lean4

theorem derivativeFinsupp_derivative (p : R[X]) :
    derivativeFinsupp (derivative p) = (derivativeFinsupp p).comapDomain Nat.succ Nat.succ_injective.injOn :=
  by
  ext i : 1
  simp

Похожие утверждения