∀ {𝕜 : Type u_1} (E : Type u_2) [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedRing E] [inst_2 : NormedAlgebra 𝕜 E]
  (c : ℕ → 𝕜) [NormOneClass E] {r : ENNReal},
  Filter.Tendsto (fun n => ENNReal.ofReal ‖c n.succ‖ / ENNReal.ofReal ‖c n‖) Filter.atTop (nhds r) →
    (FormalMultilinearSeries.ofScalars E c).radius = r⁻¹