src/HOL/Rings.thy
changeset 35083 3246e66b0874
parent 35050 9f841f20dca6
child 35092 cfe605c54e50
     1.1 --- a/src/HOL/Rings.thy	Wed Feb 10 08:49:25 2010 +0100
     1.2 +++ b/src/HOL/Rings.thy	Wed Feb 10 08:49:26 2010 +0100
     1.3 @@ -410,9 +410,14 @@
     1.4  
     1.5  end
     1.6  
     1.7 +class inverse =
     1.8 +  fixes inverse :: "'a \<Rightarrow> 'a"
     1.9 +    and divide :: "'a \<Rightarrow> 'a \<Rightarrow> 'a"  (infixl "'/" 70)
    1.10 +
    1.11  class division_ring = ring_1 + inverse +
    1.12    assumes left_inverse [simp]:  "a \<noteq> 0 \<Longrightarrow> inverse a * a = 1"
    1.13    assumes right_inverse [simp]: "a \<noteq> 0 \<Longrightarrow> a * inverse a = 1"
    1.14 +  assumes divide_inverse: "a / b = a * inverse b"
    1.15  begin
    1.16  
    1.17  subclass ring_1_no_zero_divisors