|
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 |