src/HOL/Complex.thy
changeset 44711 cd8dbfc272df
parent 44319 806e0390de53
child 44712 1e490e891c88
     1.1 --- a/src/HOL/Complex.thy	Sun Sep 04 09:49:45 2011 -0700
     1.2 +++ b/src/HOL/Complex.thy	Sun Sep 04 10:05:52 2011 -0700
     1.3 @@ -736,12 +736,6 @@
     1.4  lemma sin_n_Im_cis_pow_n: "sin (real n * a) = Im(cis a ^ n)"
     1.5  by (auto simp add: DeMoivre)
     1.6  
     1.7 -lemma expi_add: "expi(a + b) = expi(a) * expi(b)"
     1.8 -  by (rule exp_add) (* FIXME: redundant *)
     1.9 -
    1.10 -lemma expi_zero: "expi (0::complex) = 1"
    1.11 -  by (rule exp_zero) (* FIXME: redundant *)
    1.12 -
    1.13  lemma complex_expi_Ex: "\<exists>a r. z = complex_of_real r * expi a"
    1.14  apply (insert rcis_Ex [of z])
    1.15  apply (auto simp add: expi_def rcis_def mult_assoc [symmetric])