mathlib3

62297cf0 - feat(analysis/complex/cauchy_integral, analysis/analytic/basic): entire functions have power series with infinite radius of convergence (#11948)

feat(analysis/complex/cauchy_integral, analysis/analytic/basic): entire functions have power series with infinite radius of convergence (#11948) This proves that a formal multilinear series `p` which represents a function `f : 𝕜 → E` on a ball of every positive radius, then `p` represents `f` on a ball of infinite radius. Consequently, it is shown that if `f : ℂ → E` is differentiable everywhere, then `cauchy_power_series f z R` represents `f` as a power series centered at `z` in the entirety of `ℂ`, regardless of `R` (assuming `0 < R`). - [x] depends on: #11896 Co-authored-by: Yury G. Kudryashov <urkud@urkud.name>