Theorem hasFPowerSeriesWithinAt_iff_of_nhds

Modification history

2026-02-11 11:08
Mathlib/Analysis/Analytic/Basic.lean
feat: lemmas for the analytic part of the proof of the Gelfond–Schneider theorem (Part 1/5) (#34836)
Added hasFPowerSeriesWithinAt_iff_of_nhdsView on Github →