summary |
shortlog |
changelog |
graph |
tags |
bookmarks |
branches |
files |
changeset |
file |
latest |
revisions |
annotate |
diff |
comparison |
raw |
help

src/HOL/NumberTheory/README

author | nipkow |

Fri, 24 Nov 2000 16:49:27 +0100 | |

changeset 10519 | ade64af4c57c |

parent 9545 | c1d9500e2927 |

permissions | -rw-r--r-- |

hide many names from Datatype_Universe.

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'. Chinese The Chinese Remainder Theorem for an arbitrary finite number of equations. (The one-equation case is included in 'IntPrimes') Uses functions for indexing. IntFact Factorial on integers and recursively defined set including all Integers from 2 up to a. Plus definition of product of finite set. 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)