src/HOL/Divides.thy
changeset 36634 f9b43d197d16
parent 35815 10e723e54076
child 37767 a2b7a20d6ea3
     1.1 --- a/src/HOL/Divides.thy	Tue May 04 08:55:34 2010 +0200
     1.2 +++ b/src/HOL/Divides.thy	Tue May 04 08:55:39 2010 +0200
     1.3 @@ -379,6 +379,8 @@
     1.4  class ring_div = semiring_div + comm_ring_1
     1.5  begin
     1.6  
     1.7 +subclass ring_1_no_zero_divisors ..
     1.8 +
     1.9  text {* Negation respects modular equivalence. *}
    1.10  
    1.11  lemma mod_minus_eq: "(- a) mod b = (- (a mod b)) mod b"