equal
deleted
inserted
replaced
204 lemma all_A_relprime: assumes "x \<in> A" shows "gcd x p = 1" |
204 lemma all_A_relprime: assumes "x \<in> A" shows "gcd x p = 1" |
205 using p_prime A_ncong_p [OF assms] |
205 using p_prime A_ncong_p [OF assms] |
206 by (simp add: cong_altdef_int) (metis gcd_int.commute prime_imp_coprime_int) |
206 by (simp add: cong_altdef_int) (metis gcd_int.commute prime_imp_coprime_int) |
207 |
207 |
208 lemma A_prod_relprime: "gcd (setprod id A) p = 1" |
208 lemma A_prod_relprime: "gcd (setprod id A) p = 1" |
209 by (metis DEADID.map_id all_A_relprime setprod_coprime_int) |
209 by (metis id_def all_A_relprime setprod_coprime_int) |
210 |
210 |
211 |
211 |
212 subsection {* Relationships Between Gauss Sets *} |
212 subsection {* Relationships Between Gauss Sets *} |
213 |
213 |
214 lemma StandardRes_inj_on_ResSet: "ResSet m X \<Longrightarrow> (inj_on (\<lambda>b. b mod m) X)" |
214 lemma StandardRes_inj_on_ResSet: "ResSet m X \<Longrightarrow> (inj_on (\<lambda>b. b mod m) X)" |