summary |
shortlog |
changelog |
graph |
tags |
bookmarks |
branches |
files |
changeset |
file |
latest |
revisions |
annotate |
diff |
comparison |
raw |
help

src/HOL/NumberTheory/README

changeset 9508 | 4d01dbf6ded7 |

child 9545 | c1d9500e2927 |

--- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/NumberTheory/README Thu Aug 03 10:46:01 2000 +0200 @@ -0,0 +1,37 @@ +IntPrimes dvd relation, GCD, Euclid's extended algorithm, primes, + congruences (all on the Integers) + Comparable to 'Primes' theory but dvd is included here + as it is not present in 'IntDiv'. Also includes extended + GCD and congruences not present in 'Primes'. + Also a few extra theorems concerning 'mod' + Maybe it should be split/merged - at least given another + name? + +Chinese The Chinese Remainder Theorem for an arbitrary finite + number of equations. (The one-equation case is included + in 'IntPrimes') + Uses functions for indicing. Maybe 'funprod' and 'funsum' + should be based on general 'fold' on indices? + +IntPowerFact Power function on Integers (exponent is still Nat), + Factorial on integers and recursively defined set + including all Integers from 2 up to a. Plus definition + of product of finite set. + Should probably be split/merged with other theories? + +BijectionRel Inductive definitions of bijections between two different + sets and between the same set. Theorem for relating + the two definitions + +EulerFermat Fermat's Little Theorem extended to Euler's Totient function. + More abstract approach than Boyer-Moore (which seems necessary + to achieve the extended version) + +WilsonRuss Wilson's Theorem following quite closely Russinoff's approach + using Boyer-Moore (using finite sets instead of lists, though) + +WilsonBij Wilson's Theorem using a more "abstract" approach based on + bijections between sets. Does not use Fermat's Little Theorem + (unlike Russinoff) + + \ No newline at end of file