src/HOL/Ring_and_Field.thy
changeset 15228 4d332d10fa3d
parent 15197 19e735596e51
child 15229 1eb23f805c06
     1.1 --- a/src/HOL/Ring_and_Field.thy	Mon Oct 04 15:25:28 2004 +0200
     1.2 +++ b/src/HOL/Ring_and_Field.thy	Mon Oct 04 15:28:03 2004 +0200
     1.3 @@ -580,12 +580,16 @@
     1.4  lemma nonzero_inverse_eq_divide: "a \<noteq> 0 ==> inverse (a::'a::field) = 1/a"
     1.5  by (simp add: divide_inverse)
     1.6  
     1.7 -lemma divide_self [simp]: "a \<noteq> 0 ==> a / (a::'a::field) = 1"
     1.8 +lemma divide_self: "a \<noteq> 0 ==> a / (a::'a::field) = 1"
     1.9    by (simp add: divide_inverse)
    1.10  
    1.11  lemma divide_zero [simp]: "a / 0 = (0::'a::{field,division_by_zero})"
    1.12  by (simp add: divide_inverse)
    1.13  
    1.14 +lemma divide_self_if [simp]:
    1.15 +     "a / (a::'a::{field,division_by_zero}) = (if a=0 then 0 else 1)"
    1.16 +  by (simp add: divide_self)
    1.17 +
    1.18  lemma divide_zero_left [simp]: "0/a = (0::'a::field)"
    1.19  by (simp add: divide_inverse)
    1.20