mathlib3

1ff56a03 - feat(analysis/analytic): a few lemmas about summability and radius (#7365)

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".