iterate_derivative_X_add_pow — Mathlib

English

Let n,k ∈ ℕ and c ∈ R. The k-th derivative of (X + C c)^n equals descFactorial(n,k) times (X + C c)^{n−k}.

Русский

Пусть n,k ∈ ℕ и c ∈ R. k-я производная от (X + C c)^n равна descFactorial(n,k)·(X + C c)^{n−k}.

LaTeX

$$$\operatorname{derivative}^{[k]}\big((X+C c)^n\big) = \operatorname{descFactorial}(n,k) \cdot (X+C c)^{n-k}$$$

Lean4

theorem iterate_derivative_X_add_pow (n k : ℕ) (c : R) :
    derivative^[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

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