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 oneequation case is included 
8 number of equations. (The oneequation 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 BoyerMoore (which seems necessary 
20 More abstract approach than BoyerMoore (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 BoyerMoore (using finite sets instead of lists, though) 
24 using BoyerMoore (using finite sets instead of lists, though) 