equal
deleted
inserted
replaced
380 then show "a = b \<or> a = - b" |
380 then show "a = b \<or> a = - b" |
381 by (simp add: right_minus_eq eq_neg_iff_add_eq_0) |
381 by (simp add: right_minus_eq eq_neg_iff_add_eq_0) |
382 next |
382 next |
383 assume "a = b \<or> a = - b" |
383 assume "a = b \<or> a = - b" |
384 then show "a * a = b * b" by auto |
384 then show "a * a = b * b" by auto |
|
385 qed |
|
386 |
|
387 lemma dvd_mult_cancel_right [simp]: |
|
388 "a * c dvd b * c \<longleftrightarrow> c = 0 \<or> a dvd b" |
|
389 proof - |
|
390 have "a * c dvd b * c \<longleftrightarrow> (\<exists>k. b * c = (a * k) * c)" |
|
391 unfolding dvd_def by (simp add: mult_ac) |
|
392 also have "(\<exists>k. b * c = (a * k) * c) \<longleftrightarrow> c = 0 \<or> a dvd b" |
|
393 unfolding dvd_def by simp |
|
394 finally show ?thesis . |
|
395 qed |
|
396 |
|
397 lemma dvd_mult_cancel_left [simp]: |
|
398 "c * a dvd c * b \<longleftrightarrow> c = 0 \<or> a dvd b" |
|
399 proof - |
|
400 have "c * a dvd c * b \<longleftrightarrow> (\<exists>k. b * c = (a * k) * c)" |
|
401 unfolding dvd_def by (simp add: mult_ac) |
|
402 also have "(\<exists>k. b * c = (a * k) * c) \<longleftrightarrow> c = 0 \<or> a dvd b" |
|
403 unfolding dvd_def by simp |
|
404 finally show ?thesis . |
385 qed |
405 qed |
386 |
406 |
387 end |
407 end |
388 |
408 |
389 class division_ring = ring_1 + inverse + |
409 class division_ring = ring_1 + inverse + |