src/HOL/Rings.thy
 changeset 58952 5d82cdef6c1b parent 58889 5b7a9633cfa8 child 59000 6eb0725503fc
```     1.1 --- a/src/HOL/Rings.thy	Sat Nov 08 22:10:16 2014 +0100
1.2 +++ b/src/HOL/Rings.thy	Sat Nov 08 16:53:26 2014 +0100
1.3 @@ -405,11 +405,11 @@
1.4
1.5  end
1.6
1.7 -class ring_no_zero_divisors = ring + no_zero_divisors
1.8 +class semiring_no_zero_divisors = semiring_0 + no_zero_divisors
1.9  begin
1.10
1.11  lemma mult_eq_0_iff [simp]:
1.12 -  shows "a * b = 0 \<longleftrightarrow> (a = 0 \<or> b = 0)"
1.13 +  shows "a * b = 0 \<longleftrightarrow> a = 0 \<or> b = 0"
1.14  proof (cases "a = 0 \<or> b = 0")
1.15    case False then have "a \<noteq> 0" and "b \<noteq> 0" by auto
1.16      then show ?thesis using no_zero_divisors by simp
1.17 @@ -417,6 +417,11 @@
1.18    case True then show ?thesis by auto
1.19  qed
1.20
1.21 +end
1.22 +
1.23 +class ring_no_zero_divisors = ring + semiring_no_zero_divisors
1.24 +begin
1.25 +
1.26  text{*Cancellation of equalities with a common factor*}
1.27  lemma mult_cancel_right [simp]:
1.28    "a * c = b * c \<longleftrightarrow> c = 0 \<or> a = b"
1.29 @@ -434,11 +439,13 @@
1.30    thus ?thesis by simp
1.31  qed
1.32
1.33 -lemma mult_left_cancel: "c \<noteq> 0 \<Longrightarrow> (c*a=c*b) = (a=b)"
1.34 -by simp
1.35 +lemma mult_left_cancel:
1.36 +  "c \<noteq> 0 \<Longrightarrow> c * a = c * b \<longleftrightarrow> a = b"
1.37 +  by simp
1.38
1.39 -lemma mult_right_cancel: "c \<noteq> 0 \<Longrightarrow> (a*c=b*c) = (a=b)"
1.40 -by simp
1.41 +lemma mult_right_cancel:
1.42 +  "c \<noteq> 0 \<Longrightarrow> a * c = b * c \<longleftrightarrow> a = b"
1.43 +  by simp
1.44
1.45  end
1.46
```