author | wenzelm |
Wed, 10 Apr 2019 16:18:12 +0200 | |
changeset 70108 | 77f978dd8ffb |
parent 69790 | 154cf64e403e |
permissions | -rw-r--r-- |
32479 | 1 |
|
60526 | 2 |
section \<open>Comprehensive number theory\<close> |
32479 | 3 |
|
4 |
theory Number_Theory |
|
69785
9e326f6f8a24
More material for HOL-Number_Theory: ord, Carmichael's function, primitive roots
Manuel Eberl <eberlm@in.tum.de>
parents:
66276
diff
changeset
|
5 |
imports |
9e326f6f8a24
More material for HOL-Number_Theory: ord, Carmichael's function, primitive roots
Manuel Eberl <eberlm@in.tum.de>
parents:
66276
diff
changeset
|
6 |
Fib |
9e326f6f8a24
More material for HOL-Number_Theory: ord, Carmichael's function, primitive roots
Manuel Eberl <eberlm@in.tum.de>
parents:
66276
diff
changeset
|
7 |
Residues |
9e326f6f8a24
More material for HOL-Number_Theory: ord, Carmichael's function, primitive roots
Manuel Eberl <eberlm@in.tum.de>
parents:
66276
diff
changeset
|
8 |
Eratosthenes |
69790
154cf64e403e
Exponentiation by squaring, fast modular exponentiation
Manuel Eberl <eberlm@in.tum.de>
parents:
69785
diff
changeset
|
9 |
Mod_Exp |
69785
9e326f6f8a24
More material for HOL-Number_Theory: ord, Carmichael's function, primitive roots
Manuel Eberl <eberlm@in.tum.de>
parents:
66276
diff
changeset
|
10 |
Quadratic_Reciprocity |
9e326f6f8a24
More material for HOL-Number_Theory: ord, Carmichael's function, primitive roots
Manuel Eberl <eberlm@in.tum.de>
parents:
66276
diff
changeset
|
11 |
Pocklington |
9e326f6f8a24
More material for HOL-Number_Theory: ord, Carmichael's function, primitive roots
Manuel Eberl <eberlm@in.tum.de>
parents:
66276
diff
changeset
|
12 |
Prime_Powers |
9e326f6f8a24
More material for HOL-Number_Theory: ord, Carmichael's function, primitive roots
Manuel Eberl <eberlm@in.tum.de>
parents:
66276
diff
changeset
|
13 |
Residue_Primitive_Roots |
32479 | 14 |
begin |
15 |
||
16 |
end |
|
51173 | 17 |