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