equal
deleted
inserted
replaced
176 lemma zcong_zero: "[| 0 \<le> x; x < m; [x = 0](mod m) |] ==> x = 0"; |
176 lemma zcong_zero: "[| 0 \<le> x; x < m; [x = 0](mod m) |] ==> x = 0"; |
177 apply (drule order_le_imp_less_or_eq, auto) |
177 apply (drule order_le_imp_less_or_eq, auto) |
178 by (frule_tac m = m in zcong_not_zero, auto) |
178 by (frule_tac m = m in zcong_not_zero, auto) |
179 |
179 |
180 lemma all_relprime_prod_relprime: "[| finite A; \<forall>x \<in> A. (zgcd(x,y) = 1) |] |
180 lemma all_relprime_prod_relprime: "[| finite A; \<forall>x \<in> A. (zgcd(x,y) = 1) |] |
181 ==> zgcd (gsetprod id A,y) = 1"; |
181 ==> zgcd (setprod id A,y) = 1"; |
182 by (induct set: Finites, auto simp add: zgcd_zgcd_zmult) |
182 by (induct set: Finites, auto simp add: zgcd_zgcd_zmult) |
183 |
183 |
184 (*****************************************************************) |
184 (*****************************************************************) |
185 (* *) |
185 (* *) |
186 (* Some properties of MultInv *) |
186 (* Some properties of MultInv *) |