src/HOL/NumberTheory/README
 changeset 9508 4d01dbf6ded7 child 9545 c1d9500e2927
equal 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   `