changeset 9508 4d01dbf6ded7
child 9545 c1d9500e2927
equal deleted inserted replaced
9507:7903ca5fecf1 9508:4d01dbf6ded7
     1 IntPrimes	dvd relation, GCD, Euclid's extended algorithm, primes,
     2                 congruences (all on the Integers)
     3                 Comparable to 'Primes' theory but dvd is included here
     4                 as it is not present in 'IntDiv'. Also includes extended
     5                 GCD and congruences not present in 'Primes'. 
     6                 Also a few extra theorems concerning 'mod'
     7                 Maybe it should be split/merged - at least given another
     8                 name?
    10 Chinese		The Chinese Remainder Theorem for an arbitrary finite
    11                 number of equations. (The one-equation case is included
    12                 in 'IntPrimes')
    13 		Uses functions for indicing. Maybe 'funprod' and 'funsum'
    14                 should be based on general 'fold' on indices?
    16 IntPowerFact    Power function on Integers (exponent is still Nat),
    17                 Factorial on integers and recursively defined set
    18                 including all Integers from 2 up to a. Plus definition 
    19 		of product of finite set.
    20                 Should probably be split/merged with other theories?
    22 BijectionRel    Inductive definitions of bijections between two different
    23                 sets and between the same set. Theorem for relating
    24                 the two definitions
    26 EulerFermat     Fermat's Little Theorem extended to Euler's Totient function.
    27                 More abstract approach than Boyer-Moore (which seems necessary
    28                 to achieve the extended version)
    30 WilsonRuss      Wilson's Theorem following quite closely Russinoff's approach
    31 		using Boyer-Moore (using finite sets instead of lists, though)
    33 WilsonBij	Wilson's Theorem using a more "abstract" approach based on
    34 		bijections between sets.  Does not use Fermat's Little Theorem
    35                 (unlike Russinoff)