src/HOL/Rings.thy
changeset 36821 9207505d1ee5
parent 36719 d396f6f63d94
child 36970 fb3fdb4b585e
     1.1 --- a/src/HOL/Rings.thy	Mon May 10 14:53:33 2010 -0700
     1.2 +++ b/src/HOL/Rings.thy	Mon May 10 21:27:52 2010 -0700
     1.3 @@ -349,6 +349,17 @@
     1.4  class ring_1_no_zero_divisors = ring_1 + ring_no_zero_divisors
     1.5  begin
     1.6  
     1.7 +lemma square_eq_1_iff [simp]:
     1.8 +  "x * x = 1 \<longleftrightarrow> x = 1 \<or> x = - 1"
     1.9 +proof -
    1.10 +  have "(x - 1) * (x + 1) = x * x - 1"
    1.11 +    by (simp add: algebra_simps)
    1.12 +  hence "x * x = 1 \<longleftrightarrow> (x - 1) * (x + 1) = 0"
    1.13 +    by simp
    1.14 +  thus ?thesis
    1.15 +    by (simp add: eq_neg_iff_add_eq_0)
    1.16 +qed
    1.17 +
    1.18  lemma mult_cancel_right1 [simp]:
    1.19    "c = b * c \<longleftrightarrow> c = 0 \<or> b = 1"
    1.20  by (insert mult_cancel_right [of 1 c b], force)