isabelle: src/HOL/NumberTheory/README@c1d9500e2927 (annotated)

9508 4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen paulson parents: diff changeset	1	IntPrimes dvd relation, GCD, Euclid's extended algorithm, primes,
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen paulson parents: diff changeset	2	congruences (all on the Integers)
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen paulson parents: diff changeset	3	Comparable to 'Primes' theory but dvd is included here
9545 c1d9500e2927 tidied paulson parents: 9508 diff changeset	4	as it is not present in 'IntDiv'. Also includes extended
9508 4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen paulson parents: diff changeset	5	GCD and congruences not present in 'Primes'.
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen paulson parents: diff changeset	6
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen paulson parents: diff changeset	7	Chinese The Chinese Remainder Theorem for an arbitrary finite
9545 c1d9500e2927 tidied paulson parents: 9508 diff changeset	8	number of equations. (The one-equation case is included
c1d9500e2927 tidied paulson parents: 9508 diff changeset	9	in 'IntPrimes') Uses functions for indexing.
9508 4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen paulson parents: diff changeset	10
9545 c1d9500e2927 tidied paulson parents: 9508 diff changeset	11	IntFact Factorial on integers and recursively defined set
c1d9500e2927 tidied paulson parents: 9508 diff changeset	12	including all Integers from 2 up to a. Plus definition
c1d9500e2927 tidied paulson parents: 9508 diff changeset	13	of product of finite set.
9508 4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen paulson parents: diff changeset	14
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen paulson parents: diff changeset	15	BijectionRel Inductive definitions of bijections between two different
9545 c1d9500e2927 tidied paulson parents: 9508 diff changeset	16	sets and between the same set. Theorem for relating
9508 4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen paulson parents: diff changeset	17	the two definitions
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen paulson parents: diff changeset	18
9545 c1d9500e2927 tidied paulson parents: 9508 diff changeset	19	EulerFermat Fermat's Little Theorem extended to Euler's Totient function.
9508 4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen paulson parents: diff changeset	20	More abstract approach than Boyer-Moore (which seems necessary
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen paulson parents: diff changeset	21	to achieve the extended version)
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen paulson parents: diff changeset	22
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen paulson parents: diff changeset	23	WilsonRuss Wilson's Theorem following quite closely Russinoff's approach
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen paulson parents: diff changeset	24	using Boyer-Moore (using finite sets instead of lists, though)
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen paulson parents: diff changeset	25
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen paulson parents: diff changeset	26	WilsonBij Wilson's Theorem using a more "abstract" approach based on
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen paulson parents: diff changeset	27	bijections between sets. Does not use Fermat's Little Theorem
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen paulson parents: diff changeset	28	(unlike Russinoff)
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen paulson parents: diff changeset	29
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen paulson parents: diff changeset	30

author	paulson
	Mon, 07 Aug 2000 10:27:35 +0200
changeset 9545	c1d9500e2927
parent 9508	4d01dbf6ded7
permissions	-rw-r--r--