intro x
𝕜 : Type u_1
E : Type u_2
inst✝³ : NontriviallyNormedField 𝕜
inst✝² : NormedAlgebra 𝕜 ℝ
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
n : ℕ
⊢ ∀ (x : ℝ), ‖iteratedFDeriv ℝ n (fun x => cexp (x • I)) x‖ ≤ 1 * (1 + ‖x‖) ^ n
𝕜 : Type u_1
E : Type u_2
inst✝³ : NontriviallyNormedField 𝕜
inst✝² : NormedAlgebra 𝕜 ℝ
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
n : ℕ
x : ℝ
⊢ ‖iteratedFDeriv ℝ n (fun x => cexp (x • I)) x‖ ≤ 1 * (1 + ‖x‖) ^ n