| changeset 56217 | dc429a5b13c4 |
| parent 55912 | e12a0ab9917c |
| child 56480 | 093ea91498e6 |
--- a/src/HOL/Rings.thy Wed Mar 19 14:55:47 2014 +0000 +++ b/src/HOL/Rings.thy Wed Mar 19 17:06:02 2014 +0000 @@ -376,6 +376,12 @@ thus ?thesis by simp qed +lemma mult_left_cancel: "c \<noteq> 0 \<Longrightarrow> (c*a=c*b) = (a=b)" +by simp + +lemma mult_right_cancel: "c \<noteq> 0 \<Longrightarrow> (a*c=b*c) = (a=b)" +by simp + end class ring_1_no_zero_divisors = ring_1 + ring_no_zero_divisors