remove redundant lemmas i_mult_eq and i_mult_eq2 in favor of i_squared
authorhuffman
Tue Sep 06 14:53:51 2011 -0700 (2011-09-06)
changeset 44764264436dd9491
parent 44761 0694fc3248fd
child 44765 d96550db3d77
remove redundant lemmas i_mult_eq and i_mult_eq2 in favor of i_squared
src/HOL/Complex.thy
src/HOL/NSA/NSComplex.thy
     1.1 --- a/src/HOL/Complex.thy	Tue Sep 06 13:16:46 2011 -0700
     1.2 +++ b/src/HOL/Complex.thy	Tue Sep 06 14:53:51 2011 -0700
     1.3 @@ -528,12 +528,6 @@
     1.4  lemma sgn_eq: "sgn z = z / complex_of_real (cmod z)"
     1.5    by (simp add: sgn_div_norm divide_inverse scaleR_conv_of_real mult_commute)
     1.6  
     1.7 -lemma i_mult_eq: "ii * ii = complex_of_real (-1)"
     1.8 -  by (simp add: i_def complex_of_real_def)
     1.9 -
    1.10 -lemma i_mult_eq2 [simp]: "ii * ii = -(1::complex)"
    1.11 -  by (simp add: i_def complex_one_def)
    1.12 -
    1.13  lemma complex_eq_cancel_iff2 [simp]:
    1.14    shows "(Complex x y = complex_of_real xa) = (x = xa & y = 0)"
    1.15    by (simp add: complex_of_real_def)
     2.1 --- a/src/HOL/NSA/NSComplex.thy	Tue Sep 06 13:16:46 2011 -0700
     2.2 +++ b/src/HOL/NSA/NSComplex.thy	Tue Sep 06 14:53:51 2011 -0700
     2.3 @@ -163,8 +163,8 @@
     2.4  apply (simp add: minus_equation_iff [of x y])
     2.5  done
     2.6  
     2.7 -lemma hcomplex_i_mult_eq [simp]: "iii * iii = - 1"
     2.8 -by transfer (rule i_mult_eq2)
     2.9 +lemma hcomplex_i_mult_eq [simp]: "iii * iii = -1"
    2.10 +by transfer (rule i_squared)
    2.11  
    2.12  lemma hcomplex_i_mult_left [simp]: "!!z. iii * (iii * z) = -z"
    2.13  by transfer (rule complex_i_mult_minus)