equal
deleted
inserted
replaced
8 imports |
8 imports |
9 Complex_Main |
9 Complex_Main |
10 "HOL-Library.Discrete" |
10 "HOL-Library.Discrete" |
11 "HOL-Library.Extended_Real" |
11 "HOL-Library.Extended_Real" |
12 "HOL-Library.Liminf_Limsup" |
12 "HOL-Library.Liminf_Limsup" |
13 "Extended_Real_Limits" |
13 Extended_Real_Limits |
14 begin |
14 begin |
15 |
15 |
16 text \<open> |
16 text \<open> |
17 The definition of the radius of convergence of a power series, |
17 The definition of the radius of convergence of a power series, |
18 various summability tests, lemmas to compute the radius of convergence etc. |
18 various summability tests, lemmas to compute the radius of convergence etc. |