iter_deriv_zpow — Mathlib

English

For n ∈ ℕ, k ∈ ℕ, the k-th derivative (via iteration) of x^n is (∏_{i=0}^{k-1} (n−i)) x^{n−k}.

Русский

Для целого n и натурального k, k-й производной по x от x^n равна (∏_{i=0}^{k-1} (n−i)) x^{n−k}.

LaTeX

$$$\\bigl(\\mathrm{deriv}^{[k]} (x \\mapsto x^n)\\bigr)(x) = \\Big(\\prod_{i=0}^{k-1} (n - i)\\Big) x^{n-k}$$$

Lean4

theorem iter_deriv_zpow (m : ℤ) (x : 𝕜) (k : ℕ) :
    deriv^[k] (fun y => y ^ m) x = (∏ i ∈ Finset.range k, ((m : 𝕜) - i)) * x ^ (m - k) :=
  congr_fun (iter_deriv_zpow' m k) x

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