| changeset 32479 | 521cc9bf2958 |
| parent 31952 | 40501bb2d57c |
| child 45917 | 1ce1bc9ff64a |
| 32478:87201c60ae7d | 32479:521cc9bf2958 |
|---|---|
3 *) |
3 *) |
4 |
4 |
5 header {* Square roots of primes are irrational *} |
5 header {* Square roots of primes are irrational *} |
6 |
6 |
7 theory Sqrt |
7 theory Sqrt |
8 imports Complex_Main |
8 imports Complex_Main "~~/src/HOL/Number_Theory/Primes" |
9 begin |
9 begin |
10 |
10 |
11 text {* |
11 text {* |
12 The square root of any prime number (including @{text 2}) is |
12 The square root of any prime number (including @{text 2}) is |
13 irrational. |
13 irrational. |