Skip to content

Commit 65eb374

Browse files
committed
chore(Analysis/Analytic): split Analytic.Basic (#26270)
Move the results on the radius of convergence from `Analytic/Basic.lean` to a new file `Analytic/ConvergenceRadius.lean`.
1 parent 595c2c6 commit 65eb374

File tree

5 files changed

+450
-431
lines changed

5 files changed

+450
-431
lines changed

Mathlib.lean

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -1336,6 +1336,7 @@ import Mathlib.Analysis.Analytic.CPolynomialDef
13361336
import Mathlib.Analysis.Analytic.ChangeOrigin
13371337
import Mathlib.Analysis.Analytic.Composition
13381338
import Mathlib.Analysis.Analytic.Constructions
1339+
import Mathlib.Analysis.Analytic.ConvergenceRadius
13391340
import Mathlib.Analysis.Analytic.Inverse
13401341
import Mathlib.Analysis.Analytic.IsolatedZeros
13411342
import Mathlib.Analysis.Analytic.IteratedFDeriv

0 commit comments

Comments
 (0)