equal
deleted
inserted
replaced
265 apply (auto simp add: field_simps) |
265 apply (auto simp add: field_simps) |
266 done |
266 done |
267 |
267 |
268 lemma cong_mult_rcancel_int: |
268 lemma cong_mult_rcancel_int: |
269 "coprime k (m::int) \<Longrightarrow> [a * k = b * k] (mod m) = [a = b] (mod m)" |
269 "coprime k (m::int) \<Longrightarrow> [a * k = b * k] (mod m) = [a = b] (mod m)" |
270 by (metis cong_altdef_int left_diff_distrib coprime_dvd_mult_iff_int gcd.commute) |
270 by (metis cong_altdef_int left_diff_distrib coprime_dvd_mult_iff gcd.commute) |
271 |
271 |
272 lemma cong_mult_rcancel_nat: |
272 lemma cong_mult_rcancel_nat: |
273 "coprime k (m::nat) \<Longrightarrow> [a * k = b * k] (mod m) = [a = b] (mod m)" |
273 "coprime k (m::nat) \<Longrightarrow> [a * k = b * k] (mod m) = [a = b] (mod m)" |
274 by (metis cong_mult_rcancel_int [transferred]) |
274 by (metis cong_mult_rcancel_int [transferred]) |
275 |
275 |
283 |
283 |
284 (* was zcong_zgcd_zmult_zmod *) |
284 (* was zcong_zgcd_zmult_zmod *) |
285 lemma coprime_cong_mult_int: |
285 lemma coprime_cong_mult_int: |
286 "[(a::int) = b] (mod m) \<Longrightarrow> [a = b] (mod n) \<Longrightarrow> coprime m n |
286 "[(a::int) = b] (mod m) \<Longrightarrow> [a = b] (mod n) \<Longrightarrow> coprime m n |
287 \<Longrightarrow> [a = b] (mod m * n)" |
287 \<Longrightarrow> [a = b] (mod m * n)" |
288 by (metis divides_mult_int cong_altdef_int) |
288 by (metis divides_mult cong_altdef_int) |
289 |
289 |
290 lemma coprime_cong_mult_nat: |
290 lemma coprime_cong_mult_nat: |
291 assumes "[(a::nat) = b] (mod m)" and "[a = b] (mod n)" and "coprime m n" |
291 assumes "[(a::nat) = b] (mod m)" and "[a = b] (mod n)" and "coprime m n" |
292 shows "[a = b] (mod m * n)" |
292 shows "[a = b] (mod m * n)" |
293 by (metis assms coprime_cong_mult_int [transferred]) |
293 by (metis assms coprime_cong_mult_int [transferred]) |