equal
deleted
inserted
replaced
122 |
122 |
123 lemmas zgcd_ac = zgcd_assoc zgcd_commute zgcd_left_commute |
123 lemmas zgcd_ac = zgcd_assoc zgcd_commute zgcd_left_commute |
124 -- {* addition is an AC-operator *} |
124 -- {* addition is an AC-operator *} |
125 |
125 |
126 lemma zgcd_zmult_distrib2: "0 \<le> k ==> k * zgcd (m, n) = zgcd (k * m, k * n)" |
126 lemma zgcd_zmult_distrib2: "0 \<le> k ==> k * zgcd (m, n) = zgcd (k * m, k * n)" |
127 by (simp del: zmult_zminus_right |
127 by (simp del: minus_mult_right [symmetric] |
128 add: zmult_zminus_right [symmetric] nat_mult_distrib zgcd_def zabs_def |
128 add: minus_mult_right nat_mult_distrib zgcd_def zabs_def |
129 mult_less_0_iff gcd_mult_distrib2 [symmetric] zmult_int [symmetric]) |
129 mult_less_0_iff gcd_mult_distrib2 [symmetric] zmult_int [symmetric]) |
130 |
130 |
131 lemma zgcd_zmult_distrib2_abs: "zgcd (k * m, k * n) = abs k * zgcd (m, n)" |
131 lemma zgcd_zmult_distrib2_abs: "zgcd (k * m, k * n) = abs k * zgcd (m, n)" |
132 by (simp add: zabs_def zgcd_zmult_distrib2) |
132 by (simp add: zabs_def zgcd_zmult_distrib2) |
133 |
133 |
363 "0 \<le> a ==> a < m ==> [a = 0] (mod m) ==> a = 0" |
363 "0 \<le> a ==> a < m ==> [a = 0] (mod m) ==> a = 0" |
364 apply (unfold zcong_def dvd_def, auto) |
364 apply (unfold zcong_def dvd_def, auto) |
365 apply (subgoal_tac "0 < m") |
365 apply (subgoal_tac "0 < m") |
366 apply (simp add: zero_le_mult_iff) |
366 apply (simp add: zero_le_mult_iff) |
367 apply (subgoal_tac "m * k < m * 1") |
367 apply (subgoal_tac "m * k < m * 1") |
368 apply (drule zmult_zless_cancel1 [THEN iffD1]) |
368 apply (drule mult_less_cancel_left [THEN iffD1]) |
369 apply (auto simp add: linorder_neq_iff) |
369 apply (auto simp add: linorder_neq_iff) |
370 done |
370 done |
371 |
371 |
372 lemma zcong_zless_unique: |
372 lemma zcong_zless_unique: |
373 "0 < m ==> (\<exists>!b. 0 \<le> b \<and> b < m \<and> [a = b] (mod m))" |
373 "0 < m ==> (\<exists>!b. 0 \<le> b \<and> b < m \<and> [a = b] (mod m))" |