src/HOL/Rings.thy
changeset 62481 b5d8e57826df
parent 62390 842917225d56
child 62608 19f87fa0cfcb
     1.1 --- a/src/HOL/Rings.thy	Tue Mar 01 10:32:55 2016 +0100
     1.2 +++ b/src/HOL/Rings.thy	Tue Mar 01 10:36:19 2016 +0100
     1.3 @@ -441,6 +441,8 @@
     1.4  
     1.5  end
     1.6  
     1.7 +class semiring_1_no_zero_divisors = semiring_1 + semiring_no_zero_divisors
     1.8 +
     1.9  class semiring_no_zero_divisors_cancel = semiring_no_zero_divisors +
    1.10    assumes mult_cancel_right [simp]: "a * c = b * c \<longleftrightarrow> c = 0 \<or> a = b"
    1.11      and mult_cancel_left [simp]: "c * a = c * b \<longleftrightarrow> c = 0 \<or> a = b"
    1.12 @@ -479,6 +481,8 @@
    1.13  class ring_1_no_zero_divisors = ring_1 + ring_no_zero_divisors
    1.14  begin
    1.15  
    1.16 +subclass semiring_1_no_zero_divisors ..
    1.17 +
    1.18  lemma square_eq_1_iff:
    1.19    "x * x = 1 \<longleftrightarrow> x = 1 \<or> x = - 1"
    1.20  proof -
    1.21 @@ -509,6 +513,11 @@
    1.22  end
    1.23  
    1.24  class semidom = comm_semiring_1_cancel + semiring_no_zero_divisors
    1.25 +begin
    1.26 +
    1.27 +subclass semiring_1_no_zero_divisors ..
    1.28 +
    1.29 +end
    1.30  
    1.31  class idom = comm_ring_1 + semiring_no_zero_divisors
    1.32  begin