Theorem: SchwartzMap.iteratedDeriv_eq_iteratedPDeriv (ForML/Util.lean)

State before:
F : Type u_1
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
n : ℕ
f : 𝓢(ℝ, F)
x : ℝ
⊢ iteratedDeriv n (⇑f) x = ((iteratedPDeriv ℝ fun x => 1) f) x
Tactic:
simp [iteratedDeriv_eq_iteratedFDeriv, iteratedPDeriv_eq_iteratedFDeriv]
State after:
no goals