Commit 2021-04-27 20:07 1ff56a03

feat(analysis/analytic): a few lemmas about summability and radius (#7365) This PR adds a few lemmas relating the radius of a formal multilinear series p to the summability of Σ ∥pₙ∥ ∥y∥ⁿ (in both ways). There isn't anything incredibly new as these are mostly special cases of existing lemmas, but I think they could be simpler to find and use. I also modified the docstring of formal_multilinear_series.radius to emphasize the difference between "Σ pₙ yⁿconverges" and "Σ ∥pₙ∥ ∥y∥ⁿ converges".