equal
deleted
inserted
replaced
753 also have "\<dots> \<longleftrightarrow> (a * b div a) * c = (c * d div c) * a" |
753 also have "\<dots> \<longleftrightarrow> (a * b div a) * c = (c * d div c) * a" |
754 using assms by (simp add: div_mult_swap) |
754 using assms by (simp add: div_mult_swap) |
755 also have "\<dots> \<longleftrightarrow> ?Q" |
755 also have "\<dots> \<longleftrightarrow> ?Q" |
756 using assms by (simp add: ac_simps) |
756 using assms by (simp add: ac_simps) |
757 finally show ?thesis . |
757 finally show ?thesis . |
|
758 qed |
|
759 |
|
760 lemma dvd_mult_imp_div: |
|
761 assumes "a * c dvd b" |
|
762 shows "a dvd b div c" |
|
763 proof (cases "c = 0") |
|
764 case True then show ?thesis by simp |
|
765 next |
|
766 case False |
|
767 from \<open>a * c dvd b\<close> obtain d where "b = a * c * d" .. |
|
768 with False show ?thesis by (simp add: mult.commute [of a] mult.assoc) |
758 qed |
769 qed |
759 |
770 |
760 |
771 |
761 text \<open>Units: invertible elements in a ring\<close> |
772 text \<open>Units: invertible elements in a ring\<close> |
762 |
773 |