src/HOL/Complex.thy
changeset 44824 34b83d981380
parent 44823 6ce95c8c0ba8
child 44825 353ddca2e4c0
     1.1 --- a/src/HOL/Complex.thy	Wed Sep 07 10:04:07 2011 -0700
     1.2 +++ b/src/HOL/Complex.thy	Wed Sep 07 18:47:55 2011 -0700
     1.3 @@ -656,15 +656,8 @@
     1.4  lemma complex_i_mult_minus [simp]: "ii * (ii * x) = - x"
     1.5    by (simp add: mult_assoc [symmetric])
     1.6  
     1.7 -
     1.8 -lemma cis_real_of_nat_Suc_mult:
     1.9 -   "cis (real (Suc n) * a) = cis a * cis (real n * a)"
    1.10 -  by (simp add: cis_def real_of_nat_Suc left_distrib cos_add sin_add right_distrib)
    1.11 -
    1.12  lemma DeMoivre: "(cis a) ^ n = cis (real n * a)"
    1.13 -apply (induct_tac "n")
    1.14 -apply (auto simp add: cis_real_of_nat_Suc_mult)
    1.15 -done
    1.16 +  by (induct n, simp_all add: real_of_nat_Suc algebra_simps cis_mult)
    1.17  
    1.18  lemma DeMoivre2: "(rcis r a) ^ n = rcis (r ^ n) (real n * a)"
    1.19    by (simp add: rcis_def power_mult_distrib DeMoivre)