iteratedDeriv_neg — Mathlib

English

For c ∈ 𝕜, the nth iterated derivative within s of c • f equals c times the nth iterated derivative within s of f.

Русский

Для константы c в 𝕜 n-я повторная производная внутри s от c • f равна c умножить на n-ую повторную производную внутри s от f.

LaTeX

$$$\\operatorname{iteratedDerivWithin}_n (c \\cdot f) s x = c \\cdot \\operatorname{iteratedDerivWithin}_n f s x$$

Lean4

theorem iteratedDeriv_neg (n : ℕ) (f : 𝕜 → F) (a : 𝕜) : iteratedDeriv n (-f) a = -(iteratedDeriv n f a) := by
  simpa only [← iteratedDerivWithin_univ] using iteratedDerivWithin_neg f

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