| changeset 30738 | 0842e906300c |
| parent 30242 | aea5d7fa7ef5 |
| child 31044 | 6896c2498ac0 |
| 30737:9ffd27558916 | 30738:0842e906300c |
|---|---|
4 *) |
4 *) |
5 |
5 |
6 header {* Primality on nat *} |
6 header {* Primality on nat *} |
7 |
7 |
8 theory Primes |
8 theory Primes |
9 imports Plain "~~/src/HOL/ATP_Linkup" "~~/src/HOL/GCD" "~~/src/HOL/Parity" |
9 imports Complex_Main |
10 begin |
10 begin |
11 |
11 |
12 definition |
12 definition |
13 coprime :: "nat => nat => bool" where |
13 coprime :: "nat => nat => bool" where |
14 "coprime m n \<longleftrightarrow> gcd m n = 1" |
14 "coprime m n \<longleftrightarrow> gcd m n = 1" |