Cauchy-Hadamard

Stream: condensed mathematics

[Filippo A. E. Nuccio]

Do we have the Cauchy-Hadamard criterion in mathlib saying that the radius of convergence of a power series is the $\limsup$ of the absolute values of its coefficients? I cannot even find the root test for summability, actually (the ratio test is there).

[Eric Rodriguez]

docs#formal_multilinear_series.radius_eq_liminf maybe?

[Filippo A. E. Nuccio]

Lovely! Thanks.