rw [norm_smul, mul_rotate' _ ‖_ ^ n‖, mul_rotate' _ ‖_ ^ n‖]
F : Type u_1
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℂ F
inst✝ : CompleteSpace F
k n : ℕ
f : 𝓢(ℝ, F)
ξ : ℝ
⊢ (2 * π) ^ k * (|ξ| ^ k * ‖(-(2 * ↑π * I)) ^ n • 𝓕 (fun x => x ^ n • f x) ξ‖) =
    (2 * π) ^ n * ‖𝓕 (fun x => iteratedDeriv k (fun y => y ^ n • f y) x) ξ‖
F : Type u_1
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℂ F
inst✝ : CompleteSpace F
k n : ℕ
f : 𝓢(ℝ, F)
ξ : ℝ
⊢ ‖(-(2 * ↑π * I)) ^ n‖ * (‖𝓕 (fun x => x ^ n • f x) ξ‖ * |ξ| ^ k * (2 * π) ^ k) =
    (2 * π) ^ n * ‖𝓕 (fun x => iteratedDeriv k (fun y => y ^ n • f y) x) ξ‖