derivative_pow — Mathlib

English

For any natural numbers n and k, derivative^[k](X^n) = (n.descFactorial k) cast as a scalar times X^{n−k}.

Русский

Для любых n, k ∈ ℕ, derivative^[k](X^n) = (n.descFactorial k) в виде скалярного множителя умноженное на X^{n−k}.

LaTeX

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

Lean4

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]

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