equal
deleted
inserted
replaced
5 *) |
5 *) |
6 |
6 |
7 header{*Existence of Nth Root*} |
7 header{*Existence of Nth Root*} |
8 |
8 |
9 theory NthRoot |
9 theory NthRoot |
10 import SEQ HSeries |
10 imports SEQ HSeries |
11 begin |
11 begin |
12 |
12 |
13 text {* |
13 text {* |
14 Various lemmas needed for this result. We follow the proof given by |
14 Various lemmas needed for this result. We follow the proof given by |
15 John Lindsay Orr (\texttt{jorr@math.unl.edu}) in his Analysis |
15 John Lindsay Orr (\texttt{jorr@math.unl.edu}) in his Analysis |