Theorem one_add_rpow_hasFPowerSeriesOnBall_zero

Modification history

2025-12-10 16:38
Mathlib/Analysis/Analytic/Binomial.lean
feat(Analysis): `HasFPowerSeriesOnBall (fun x ↦ 1 / (1 - x))` and friends (#32373)
Deleted one_add_rpow_hasFPowerSeriesOnBall_zeroView on Github →
2025-11-06 19:26
Mathlib/Analysis/Analytic/Binomial.lean
feat(Analysis): binomial series convergence (#31047) …
Added one_add_rpow_hasFPowerSeriesOnBall_zeroView on Github →