no goals
𝕜 : Type u_3
E : Type u_1
F : Type u_2
G : Type ?u.62997
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✝ C r : ℝ≥0
h : ∀ (n : ℕ), ‖p n‖₊ * r ^ n ≤ C
n : ℕ
⊢ ‖p n‖ * ↑r ^ n ≤ ↑C
exact_mod_cast h n