iteratedDeriv_const_smul — Mathlib

English

For scalar c, the nth iterated derivative within s of c • f equals c • iteratedDeriv within of f, with casted n.

Русский

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

LaTeX

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

Lean4

theorem iteratedDeriv_const_smul {n : ℕ} {f : 𝕜 → F} (h : ContDiffAt 𝕜 n f x) (c : 𝕜) :
    iteratedDeriv n (c • f) x = c • iteratedDeriv n f x := by
  simpa only [iteratedDerivWithin_univ] using
    iteratedDerivWithin_const_smul (Set.mem_univ x) uniqueDiffOn_univ c (contDiffWithinAt_univ.mpr h)

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