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

src/HOL/NumberTheory/README

changeset 9545 | c1d9500e2927 |

parent 9508 | 4d01dbf6ded7 |

--- a/src/HOL/NumberTheory/README Mon Aug 07 10:27:11 2000 +0200 +++ b/src/HOL/NumberTheory/README Mon Aug 07 10:27:35 2000 +0200 @@ -1,29 +1,22 @@ 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 + 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? + number of equations. (The one-equation case is included + in 'IntPrimes') Uses functions for indexing. -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? +IntFact Factorial on integers and recursively defined set + including all Integers from 2 up to a. Plus definition + of product of finite set. BijectionRel Inductive definitions of bijections between two different - sets and between the same set. Theorem for relating + sets and between the same set. Theorem for relating the two definitions -EulerFermat Fermat's Little Theorem extended to Euler's Totient function. +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)