no goals
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type ?u.103270
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
v : F
⊢ ∀ (m : ℕ), constFormalMultilinearSeries 𝕜 E v (m + 1) = 0
simp [constFormalMultilinearSeries]