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