Theorem Real.hasFPowerSeriesOnBall_ofScalars_mul_add_zero

Modification history

2026-01-07 13:28
Mathlib/Analysis/Analytic/Binomial.lean
feat(Analysis): ℘ is analytic (#32911)
Added Real.hasFPowerSeriesOnBall_ofScalars_mul_add_zeroView on Github →