# Representation of formal_multilinear_series.radius as a liminf#
In this file we prove that the radius of convergence of a formal_multilinear_series is equal to $\liminf_{n\to\infty} \frac{1}{\sqrt[n]{∥p n∥}}$. This lemma can't go to basic.lean because this would create a circular dependency once we redefine exp using formal_multilinear_series.
The radius of a formal multilinear series is equal to $\liminf_{n\to\infty} \frac{1}{\sqrt[n]{∥p n∥}}$. The actual statement uses ℝ≥0 and some coercions.