src/HOL/Rings.thy
changeset 44346 00dd3c4dabe0
parent 44064 5bce8ff0d9ae
child 44350 63cddfbc5a09
     1.1 --- a/src/HOL/Rings.thy	Sat Aug 20 09:59:28 2011 -0700
     1.2 +++ b/src/HOL/Rings.thy	Sat Aug 20 10:08:47 2011 -0700
     1.3 @@ -277,6 +277,10 @@
     1.4  
     1.5  subclass semiring_1_cancel ..
     1.6  
     1.7 +lemma square_diff_one_factored:
     1.8 +  "x * x - 1 = (x + 1) * (x - 1)"
     1.9 +  by (simp add: algebra_simps)
    1.10 +
    1.11  end
    1.12  
    1.13  class comm_ring_1 = comm_ring + zero_neq_one + comm_monoid_mult