| changeset 27368 | 9f90ac19e32b |
| parent 27106 | ff27dc6e7d05 |
| child 27487 | c8a6ce181805 |
| 27367:a75d71c73362 | 27368:9f90ac19e32b |
|---|---|
5 *) |
5 *) |
6 |
6 |
7 header {* Primality on nat *} |
7 header {* Primality on nat *} |
8 |
8 |
9 theory Primes |
9 theory Primes |
10 imports GCD Parity |
10 imports Plain ATP_Linkup GCD Parity |
11 begin |
11 begin |
12 |
12 |
13 definition |
13 definition |
14 coprime :: "nat => nat => bool" where |
14 coprime :: "nat => nat => bool" where |
15 "coprime m n \<longleftrightarrow> (gcd (m, n) = 1)" |
15 "coprime m n \<longleftrightarrow> (gcd (m, n) = 1)" |