equal
deleted
inserted
replaced
23 |
23 |
24 lemma odd_p: "odd p" |
24 lemma odd_p: "odd p" |
25 using p_ge_2 p_prime prime_odd_nat by blast |
25 using p_ge_2 p_prime prime_odd_nat by blast |
26 |
26 |
27 lemma p_ge_0: "0 < int p" |
27 lemma p_ge_0: "0 < int p" |
28 using p_prime not_prime_0[where 'a = nat] by fastforce+ |
28 by (simp add: p_prime prime_gt_0_nat) |
29 |
29 |
30 lemma p_eq2: "int p = (2 * ((int p - 1) div 2)) + 1" |
30 lemma p_eq2: "int p = (2 * ((int p - 1) div 2)) + 1" |
31 using odd_p by simp |
31 using odd_p by simp |
32 |
32 |
33 lemma odd_q: "odd q" |
33 lemma odd_q: "odd q" |
34 using q_ge_2 q_prime prime_odd_nat by blast |
34 using q_ge_2 q_prime prime_odd_nat by blast |
35 |
35 |
36 lemma q_ge_0: "0 < int q" |
36 lemma q_ge_0: "0 < int q" |
37 using q_prime not_prime_0[where 'a = nat] by fastforce+ |
37 by (simp add: q_prime prime_gt_0_nat) |
38 |
38 |
39 lemma q_eq2: "int q = (2 * ((int q - 1) div 2)) + 1" |
39 lemma q_eq2: "int q = (2 * ((int q - 1) div 2)) + 1" |
40 using odd_q by simp |
40 using odd_q by simp |
41 |
41 |
42 lemma pq_eq2: "int p * int q = (2 * ((int p * int q - 1) div 2)) + 1" |
42 lemma pq_eq2: "int p * int q = (2 * ((int p * int q - 1) div 2)) + 1" |
91 definition "e = card E" |
91 definition "e = card E" |
92 definition "f = card F" |
92 definition "f = card F" |
93 |
93 |
94 lemma Gpq: "GAUSS p q" |
94 lemma Gpq: "GAUSS p q" |
95 using p_prime pq_neq p_ge_2 q_prime |
95 using p_prime pq_neq p_ge_2 q_prime |
96 by (auto simp: GAUSS_def cong_altdef_int zdvd_int [symmetric] dest: primes_dvd_imp_eq) |
96 by (auto simp: GAUSS_def cong_altdef_int dest: primes_dvd_imp_eq) |
97 |
97 |
98 lemma Gqp: "GAUSS q p" |
98 lemma Gqp: "GAUSS q p" |
99 by (simp add: QRqp QR.Gpq) |
99 by (simp add: QRqp QR.Gpq) |
100 |
100 |
101 lemma QR_lemma_01: "(\<lambda>x. x mod q) ` E = GAUSS.E q p" |
101 lemma QR_lemma_01: "(\<lambda>x. x mod q) ` E = GAUSS.E q p" |