iter_deriv_pow' — Mathlib

English

A variant of the iterated derivative for natural indices: (deriv^[k] x^n) equals the product term times x^{n-k}.

Русский

Вариант итеративной формулы для натуральных индексов: (deriv^[k] x^n) = Продукт(0..k-1) (n−i) · x^{n−k}.

LaTeX

$$$\\text{iter\_deriv\_pow'} (n, k) : (\\mathrm{deriv}^[k] (x \\mapsto x^n)) = (\\prod_{i=0}^{k-1} (n - i)) \\cdot x^{n-k}$$$

Lean4

@[simp]
theorem iter_deriv_pow' (n k : ℕ) :
    (deriv^[k] fun x : 𝕜 => x ^ n) = fun x => (∏ i ∈ Finset.range k, ((n : 𝕜) - i)) * x ^ (n - k) :=
  funext fun x => iter_deriv_pow n x k

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