tuned
authorhuffman
Thu Sep 08 07:06:59 2011 -0700 (2011-09-08)
changeset 44841e55503200061
parent 44840 38975527c757
child 44842 282eef2c0f77
tuned
src/HOL/Complex.thy
     1.1 --- a/src/HOL/Complex.thy	Thu Sep 08 11:31:53 2011 +0200
     1.2 +++ b/src/HOL/Complex.thy	Thu Sep 08 07:06:59 2011 -0700
     1.3 @@ -253,6 +253,10 @@
     1.4    shows "complex_of_real r * Complex x y = Complex (r*x) (r*y)"
     1.5    by (simp add: complex_of_real_def)
     1.6  
     1.7 +lemma complex_eq_cancel_iff2 [simp]:
     1.8 +  shows "(Complex x y = complex_of_real xa) = (x = xa & y = 0)"
     1.9 +  by (simp add: complex_of_real_def)
    1.10 +
    1.11  lemma complex_split_polar:
    1.12       "\<exists>r a. z = complex_of_real r * (Complex (cos a) (sin a))"
    1.13    by (simp add: complex_eq_iff polar_Ex)
    1.14 @@ -539,10 +543,6 @@
    1.15  lemma sgn_eq: "sgn z = z / complex_of_real (cmod z)"
    1.16    by (simp add: sgn_div_norm divide_inverse scaleR_conv_of_real mult_commute)
    1.17  
    1.18 -lemma complex_eq_cancel_iff2 [simp]:
    1.19 -  shows "(Complex x y = complex_of_real xa) = (x = xa & y = 0)"
    1.20 -  by (simp add: complex_of_real_def)
    1.21 -
    1.22  lemma Re_sgn [simp]: "Re(sgn z) = Re(z)/cmod z"
    1.23    by (simp add: complex_sgn_def divide_inverse)
    1.24