isabelle: src/HOL/Number_Theory/Number_Theory.thy@77cbf472fcc9 (annotated)

32479 521cc9bf2958 some reorganization of number theory haftmann parents: diff changeset	1
60526 fad653acf58f isabelle update_cartouches; wenzelm parents: 58889 diff changeset	2	section \<open>Comprehensive number theory\<close>
32479 521cc9bf2958 some reorganization of number theory haftmann parents: diff changeset	3
521cc9bf2958 some reorganization of number theory haftmann parents: diff changeset	4	theory Number_Theory
69785 9e326f6f8a24 More material for HOL-Number_Theory: ord, Carmichael's function, primitive roots Manuel Eberl <eberlm@in.tum.de> parents: 66276 diff changeset	5	imports
9e326f6f8a24 More material for HOL-Number_Theory: ord, Carmichael's function, primitive roots Manuel Eberl <eberlm@in.tum.de> parents: 66276 diff changeset	6	Fib
9e326f6f8a24 More material for HOL-Number_Theory: ord, Carmichael's function, primitive roots Manuel Eberl <eberlm@in.tum.de> parents: 66276 diff changeset	7	Residues
9e326f6f8a24 More material for HOL-Number_Theory: ord, Carmichael's function, primitive roots Manuel Eberl <eberlm@in.tum.de> parents: 66276 diff changeset	8	Eratosthenes
69790 154cf64e403e Exponentiation by squaring, fast modular exponentiation Manuel Eberl <eberlm@in.tum.de> parents: 69785 diff changeset	9	Mod_Exp
69785 9e326f6f8a24 More material for HOL-Number_Theory: ord, Carmichael's function, primitive roots Manuel Eberl <eberlm@in.tum.de> parents: 66276 diff changeset	10	Quadratic_Reciprocity
9e326f6f8a24 More material for HOL-Number_Theory: ord, Carmichael's function, primitive roots Manuel Eberl <eberlm@in.tum.de> parents: 66276 diff changeset	11	Pocklington
9e326f6f8a24 More material for HOL-Number_Theory: ord, Carmichael's function, primitive roots Manuel Eberl <eberlm@in.tum.de> parents: 66276 diff changeset	12	Prime_Powers
9e326f6f8a24 More material for HOL-Number_Theory: ord, Carmichael's function, primitive roots Manuel Eberl <eberlm@in.tum.de> parents: 66276 diff changeset	13	Residue_Primitive_Roots
32479 521cc9bf2958 some reorganization of number theory haftmann parents: diff changeset	14	begin
521cc9bf2958 some reorganization of number theory haftmann parents: diff changeset	15
521cc9bf2958 some reorganization of number theory haftmann parents: diff changeset	16	end
51173 3cbb4e95a565 Sieve of Eratosthenes haftmann parents: 32479 diff changeset	17

author	blanchet
	Thu, 18 Aug 2022 09:29:11 +0200
changeset 75874	77cbf472fcc9
parent 69790	154cf64e403e
child 82518	da14e77a48b2
permissions	-rw-r--r--