Commit 2026-02-11 11:08 11639775

View on Github →

feat: lemmas for the analytic part of the proof of the Gelfond–Schneider theorem (Part 1/5) (#34836)

Estimated changes

Modified Mathlib/Analysis/Analytic/Basic.lean

added theorem AnalyticOn.analyticAt

added theorem analyticOn_congr

added theorem hasFPowerSeriesWithinAt_iff_of_nhds