simp
case zero
F : Type u_1
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℂ F
inst✝ : CompleteSpace F
f : 𝓢(ℝ, F)
ξ : ℝ
⊢ 𝓕 (fun x => iteratedDeriv Nat.zero (fun y => f y) x) ξ = (2 * ↑π * I * ↑ξ) ^ Nat.zero • 𝓕 (fun x => f x) ξ
no goals