equal
deleted
inserted
replaced
4 Conversion to Isar and new proofs by Lawrence C Paulson, 2004 |
4 Conversion to Isar and new proofs by Lawrence C Paulson, 2004 |
5 *) |
5 *) |
6 |
6 |
7 header{*Existence of Nth Root*} |
7 header{*Existence of Nth Root*} |
8 |
8 |
9 theory NthRoot = SEQ + HSeries: |
9 theory NthRoot |
|
10 import SEQ HSeries |
|
11 begin |
10 |
12 |
11 text {* |
13 text {* |
12 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 |
13 John Lindsay Orr (\texttt{jorr@math.unl.edu}) in his Analysis |
15 John Lindsay Orr (\texttt{jorr@math.unl.edu}) in his Analysis |
14 Webnotes available at \url{http://www.math.unl.edu/~webnotes}. |
16 Webnotes available at \url{http://www.math.unl.edu/~webnotes}. |