summary |
shortlog |
changelog |
graph |
tags |
bookmarks |
branches |
files |
changeset |
file |
latest |
revisions |
annotate |
diff |
comparison |
raw |
help

src/HOL/Rings.thy

changeset 60570 | 7ed2cde6806d |

parent 60562 | 24af00b010cf |

child 60615 | e5fa1d5d3952 |

--- a/src/HOL/Rings.thy Thu Jun 25 15:01:41 2015 +0200 +++ b/src/HOL/Rings.thy Thu Jun 25 15:01:42 2015 +0200 @@ -619,6 +619,16 @@ shows "a div a = 1" using assms nonzero_mult_divide_cancel_left [of a 1] by simp +lemma divide_zero_left [simp]: + "0 div a = 0" +proof (cases "a = 0") + case True then show ?thesis by simp +next + case False then have "a * 0 div a = 0" + by (rule nonzero_mult_divide_cancel_left) + then show ?thesis by simp +qed + end class idom_divide = idom + semidom_divide @@ -651,6 +661,16 @@ shows "b div c * a = (b * a) div c" using assms div_mult_swap [of c b a] by (simp add: ac_simps) +lemma dvd_div_mult2_eq: + assumes "b * c dvd a" + shows "a div (b * c) = a div b div c" +using assms proof + fix k + assume "a = b * c * k" + then show ?thesis + by (cases "b = 0 \<or> c = 0") (auto, simp add: ac_simps) +qed + text \<open>Units: invertible elements in a ring\<close> @@ -803,6 +823,17 @@ with assms show ?thesis by simp qed +lemma is_unit_div_mult2_eq: + assumes "is_unit b" and "is_unit c" + shows "a div (b * c) = a div b div c" +proof - + from assms have "is_unit (b * c)" by (simp add: unit_prod) + then have "b * c dvd a" + by (rule unit_imp_dvd) + then show ?thesis + by (rule dvd_div_mult2_eq) +qed + text \<open>Associated elements in a ring --- an equivalence relation induced by the quasi-order divisibility.\<close>