equal
deleted
inserted
replaced
5 *) |
5 *) |
6 |
6 |
7 header {* Nth Roots of Real Numbers *} |
7 header {* Nth Roots of Real Numbers *} |
8 |
8 |
9 theory NthRoot |
9 theory NthRoot |
10 imports Parity "../Hyperreal/Deriv" |
10 imports "~~/src/HOL/Library/Parity" "../Hyperreal/Deriv" |
11 begin |
11 begin |
12 |
12 |
13 subsection {* Existence of Nth Root *} |
13 subsection {* Existence of Nth Root *} |
14 |
14 |
15 text {* Existence follows from the Intermediate Value Theorem *} |
15 text {* Existence follows from the Intermediate Value Theorem *} |