author | eberlm <eberlm@in.tum.de> |
Sat, 15 Jul 2017 14:32:02 +0100 | |
changeset 66276 | acc3b7dd0b21 |
parent 64318 | 1e92b5c35615 |
child 69785 | 9e326f6f8a24 |
permissions | -rw-r--r-- |
32479 | 1 |
|
60526 | 2 |
section \<open>Comprehensive number theory\<close> |
32479 | 3 |
|
4 |
theory Number_Theory |
|
66276
acc3b7dd0b21
More material on powers for HOL-Computational_Algebra/HOL-Number_Theory
eberlm <eberlm@in.tum.de>
parents:
64318
diff
changeset
|
5 |
imports Fib Residues Eratosthenes Quadratic_Reciprocity Pocklington Prime_Powers |
32479 | 6 |
begin |
7 |
||
8 |
end |
|
51173 | 9 |