iterate_derivative_sub — Mathlib

English

For any f,g and k, derivative iterated k times of f − g equals derivative iterated k times of f minus derivative iterated k times of g.

Русский

Для любых f,g и 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_sub {k : ℕ} {f g : R[X]} : derivative^[k] (f - g) = derivative^[k] f - derivative^[k] g :=
  iterate_map_sub derivative k f g

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