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'. |
6 Also a few extra theorems concerning 'mod' |
|
7 Maybe it should be split/merged - at least given another |
|
8 name? |
|
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) |