Commit 7d753933 by wenzelm

### import from ~~/src/HOL/Number_Theory, not old NumberTheory (Why was this never detected?);

parent 740b1087f9c7
 ... ... @@ -125,7 +125,7 @@ one of the standard images like HOL, use something like the following: \begin{verbatim} theory MyTheory imports "~~/src/HOL/NumberTheory" imports "~~/src/HOL/Number_Theory/Number_Theory" begin \end{verbatim} *} ... ...
 ... ... @@ -7,8 +7,8 @@ header {* Powers, prime numbers and divisibility *} theory IntNatAux imports "~~/src/HOL/NumberTheory/Factorization" "~~/src/HOL/NumberTheory/EvenOdd" "~~/src/HOL/Number_Theory/Factorization" "~~/src/HOL/Number_Theory/EvenOdd" begin text {* Contains lemmas about divisibility and coprimality of powers, as well as some results about parities and small powers. Most lemmas are developed for the integers as well as for the natural numbers. *} ... ...
 ... ... @@ -7,7 +7,7 @@ header {* The quadratic form $x^2 + Ny^2$ *} theory QuadForm imports "~~/src/HOL/NumberTheory/Quadratic_Reciprocity" "~~/src/HOL/Number_Theory/Quadratic_Reciprocity" IntNatAux begin ... ...
 ... ... @@ -7,7 +7,7 @@ header {* Lagrange's four-square theorem *} theory FourSquares imports "../Fermat3_4/IntNatAux" "~~/src/HOL/NumberTheory/Quadratic_Reciprocity" "~~/src/HOL/Number_Theory/Quadratic_Reciprocity" begin text {* Shows that all nonnegative integers can be written as the sum of four squares. The proof consists of the following steps: ... ...
 ... ... @@ -7,7 +7,7 @@ header {* Sums of two squares *} theory TwoSquares imports "../Fermat3_4/IntNatAux" "~~/src/HOL/NumberTheory/Euler" "~~/src/HOL/Number_Theory/Euler" begin text {* Show that $(\frac{-1}{p}) = +1$ for primes $p \equiv 1 \bmod 4$. *} ... ...
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment