IntPrimes dvd relation, GCD, Euclid's extended algorithm, primes,
congruences (all on the Integers)
Comparable to 'Primes' theory but dvd is included here
as it is not present in 'IntDiv'. Also includes extended
GCD and congruences not present in 'Primes'.
Also a few extra theorems concerning 'mod'
Maybe it should be split/merged - at least given another
name?
Chinese The Chinese Remainder Theorem for an arbitrary finite
number of equations. (The one-equation case is included
in 'IntPrimes')
Uses functions for indicing. Maybe 'funprod' and 'funsum'
should be based on general 'fold' on indices?
IntPowerFact Power function on Integers (exponent is still Nat),
Factorial on integers and recursively defined set
including all Integers from 2 up to a. Plus definition
of product of finite set.
Should probably be split/merged with other theories?
BijectionRel Inductive definitions of bijections between two different
sets and between the same set. Theorem for relating
the two definitions
EulerFermat Fermat's Little Theorem extended to Euler's Totient function.
More abstract approach than Boyer-Moore (which seems necessary
to achieve the extended version)
WilsonRuss Wilson's Theorem following quite closely Russinoff's approach
using Boyer-Moore (using finite sets instead of lists, though)
WilsonBij Wilson's Theorem using a more "abstract" approach based on
bijections between sets. Does not use Fermat's Little Theorem
(unlike Russinoff)