no goals
𝕜 : Type u_3
E : Type u_1
F : Type u_2
G : Type ?u.93541
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
p : FormalMultilinearSeries 𝕜 E F
r✝ : ℝ≥0
h : ∀ᶠ (n : ℕ) in atTop, p n = 0
r : ℝ≥0
n : ℕ
hn : p n = 0
⊢ (fun _x => 0) n = (fun n => ‖p n‖ * ↑r ^ n) n
simp [hn]