Theorem Real.hasFPowerSeriesOnBall_linear_zero

Modification history

2026-01-07 13:28

Mathlib/Analysis/Analytic/Binomial.lean

feat(Analysis): ℘ is analytic (#32911)

Deleted Real.hasFPowerSeriesOnBall_linear_zero View on Github →

2025-12-10 16:38

Mathlib/Analysis/Analytic/Binomial.lean

feat(Analysis): `HasFPowerSeriesOnBall (fun x ↦ 1 / (1 - x))` and friends (#32373)

Added Real.hasFPowerSeriesOnBall_linear_zero View on Github →