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