iterate_derivative_X_sub_pow_self

English

For all n,k, derivative iterated k times of f − g equals derivative iterated k times of f minus derivative iterated k times of g.

Русский

Для всех n,k, k-я производная от f − g равна k-й производной f минус k-й производной g.

LaTeX

$$$\operatorname{derivative}^{[k]}(f - g) = \operatorname{derivative}^{[k]}f - \operatorname{derivative}^{[k]}g$$$

Lean4

theorem iterate_derivative_X_sub_pow_self (n : ℕ) (c : R) : derivative^[n] ((X - C c) ^ n) = n.factorial := by
  rw [iterate_derivative_X_sub_pow, n.sub_self, pow_zero, nsmul_one, n.descFactorial_self]

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