English
Let i be a nonnegative integer and a a scalar. If f is ContDiffAt 𝕜 i at x, then the i-th iterated derivative of the constant-scalar multiple a·f at x is a times the i-th iterated derivative of f at x:
Русский
Пусть i — неотрицательное целое, a — скаляр. Если f является ContDiffAt 𝕜 i в точке x, то i-й итеративной производной от константного скалярного умножения a·f в точке x равна a·(i-я итеративная производная f в x).
LaTeX
$$$\\displaystyle\\text{If } \\mathrm{ContDiffAt}_{\\mathbb{k}}(i,f,x), \\quad \\operatorname{iteratedFDeriv}_{\\mathbb{k}}(i, a\\cdot f)(x) = a\\cdot \\operatorname{iteratedFDeriv}_{\\mathbb{k}}(i,f)(x).$$$
Lean4
theorem iteratedFDeriv_const_smul_apply (hf : ContDiffAt 𝕜 i f x) :
iteratedFDeriv 𝕜 i (a • f) x = a • iteratedFDeriv 𝕜 i f x :=
(a • (1 : F →L[𝕜] F)).iteratedFDeriv_comp_left hf le_rfl
