simp
case zero
𝕜 : Type u_1
E : Type u_2
inst✝³ : NontriviallyNormedField 𝕜
inst✝² : NormedAlgebra 𝕜 ℝ
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
x : ℝ
⊢ iteratedDeriv Nat.zero (fun x => cexp (x • I)) x = I ^ Nat.zero * cexp (x • I)
no goals