src/HOL/NumberTheory/README
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?
       
     9 
       
    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?
       
    15 
       
    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?
       
    21 
       
    22 BijectionRel    Inductive definitions of bijections between two different
       
    23                 sets and between the same set. Theorem for relating
       
    24                 the two definitions
       
    25 
       
    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)
       
    29 
       
    30 WilsonRuss      Wilson's Theorem following quite closely Russinoff's approach
       
    31 		using Boyer-Moore (using finite sets instead of lists, though)
       
    32 
       
    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)
       
    36  
       
    37