rw [← iteratedFDeriv_const_smul_apply hf]
𝕜 : Type u_1
𝕜' : Type u_2
E : Type u_3
F : Type u_4
inst✝⁸ : NontriviallyNormedField 𝕜
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace 𝕜 E
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace 𝕜 F
inst✝³ : Semiring 𝕜'
inst✝² : Module 𝕜' F
inst✝¹ : SMulCommClass 𝕜 𝕜' F
inst✝ : ContinuousConstSMul 𝕜' F
i : ℕ
a : 𝕜'
f : E → F
x : E
hf : ContDiff 𝕜 (↑i) f
⊢ iteratedFDeriv 𝕜 i (fun x => a • f x) x = a • iteratedFDeriv 𝕜 i f x
𝕜 : Type u_1
𝕜' : Type u_2
E : Type u_3
F : Type u_4
inst✝⁸ : NontriviallyNormedField 𝕜
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace 𝕜 E
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace 𝕜 F
inst✝³ : Semiring 𝕜'
inst✝² : Module 𝕜' F
inst✝¹ : SMulCommClass 𝕜 𝕜' F
inst✝ : ContinuousConstSMul 𝕜' F
i : ℕ
a : 𝕜'
f : E → F
x : E
hf : ContDiff 𝕜 (↑i) f
⊢ iteratedFDeriv 𝕜 i (fun x => a • f x) x = iteratedFDeriv 𝕜 i (a • f) x