src/HOL/Number_Theory/Gauss.thy
changeset 58288 87b59745dd6d
parent 57512 cc97b347b301
child 58410 6d46ad54a2ab
equal deleted inserted replaced
58287:10105897bc22 58288:87b59745dd6d
   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)"