src/HOL/Complex.thy
changeset 61609 77b453bd616f
parent 61552 980dd46a03fb
child 61649 268d88ec9087
     1.1 --- a/src/HOL/Complex.thy	Tue Nov 03 11:20:21 2015 +0100
     1.2 +++ b/src/HOL/Complex.thy	Tue Nov 10 14:18:41 2015 +0000
     1.3 @@ -166,7 +166,7 @@
     1.4  
     1.5  lemma Im_divide_numeral [simp]: "Im (z / numeral w) = Im z / numeral w"
     1.6    by (simp add: Im_divide sqr_conv_mult)
     1.7 -  
     1.8 +
     1.9  lemma Re_divide_of_nat: "Re (z / of_nat n) = Re z / of_nat n"
    1.10    by (cases n) (simp_all add: Re_divide divide_simps power2_eq_square del: of_nat_Suc)
    1.11  
    1.12 @@ -688,7 +688,7 @@
    1.13    by (simp add: complex_eq_iff cos_add sin_add)
    1.14  
    1.15  lemma DeMoivre: "(cis a) ^ n = cis (real n * a)"
    1.16 -  by (induct n, simp_all add: real_of_nat_Suc algebra_simps cis_mult)
    1.17 +  by (induct n, simp_all add: of_nat_Suc algebra_simps cis_mult)
    1.18  
    1.19  lemma cis_inverse [simp]: "inverse(cis a) = cis (-a)"
    1.20    by (simp add: complex_eq_iff)
    1.21 @@ -757,8 +757,7 @@
    1.22      have "\<i> ^ n = fact n *\<^sub>R (cos_coeff n + \<i> * sin_coeff n)"
    1.23        by (induct n)
    1.24           (simp_all add: sin_coeff_Suc cos_coeff_Suc complex_eq_iff Re_divide Im_divide field_simps
    1.25 -                        power2_eq_square real_of_nat_Suc add_nonneg_eq_0_iff
    1.26 -                        real_of_nat_def[symmetric])
    1.27 +                        power2_eq_square of_nat_Suc add_nonneg_eq_0_iff)
    1.28      then have "(\<i> * complex_of_real b) ^ n /\<^sub>R fact n =
    1.29          of_real (cos_coeff n * b^n) + \<i> * of_real (sin_coeff n * b^n)"
    1.30        by (simp add: field_simps) }