mathlib3

06e7f767 - feat(analysis/analytic/basic): add uniqueness results for power series (#11896)

feat(analysis/analytic/basic): add uniqueness results for power series (#11896) This establishes that if a function has two power series representations on balls of positive radius, then the corresponding formal multilinear series are equal; this is only for the one-dimensional case (i.e., for functions from the scalar field). Consequently, one may exchange the radius of convergence between these power series.