author paulson
Thu, 03 Aug 2000 10:46:01 +0200
changeset 9508 4d01dbf6ded7
child 9545 c1d9500e2927
permissions -rw-r--r--
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen

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

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)