src/HOL/Complex.thy
changeset 65578 e4997c181cce
parent 65274 db2de50de28e
child 65579 52eafedaf196
     1.1 --- a/src/HOL/Complex.thy	Tue Apr 25 08:38:23 2017 +0200
     1.2 +++ b/src/HOL/Complex.thy	Tue Apr 25 16:39:54 2017 +0100
     1.3 @@ -138,7 +138,7 @@
     1.4  end
     1.5  
     1.6  
     1.7 -subsection \<open>Numerals, Arithmetic, and Embedding from Reals\<close>
     1.8 +subsection \<open>Numerals, Arithmetic, and Embedding from \<real>\<close>
     1.9  
    1.10  abbreviation complex_of_real :: "real \<Rightarrow> complex"
    1.11    where "complex_of_real \<equiv> of_real"
    1.12 @@ -649,10 +649,10 @@
    1.13  lemma Im_divide_of_real [simp]: "Im (z / of_real r) = Im z / r"
    1.14    by (simp add: Im_divide power2_eq_square)
    1.15  
    1.16 -lemma Re_divide_Reals: "r \<in> Reals \<Longrightarrow> Re (z / r) = Re z / Re r"
    1.17 +lemma Re_divide_Reals [simp]: "r \<in> \<real> \<Longrightarrow> Re (z / r) = Re z / Re r"
    1.18    by (metis Re_divide_of_real of_real_Re)
    1.19  
    1.20 -lemma Im_divide_Reals: "r \<in> Reals \<Longrightarrow> Im (z / r) = Im z / Re r"
    1.21 +lemma Im_divide_Reals [simp]: "r \<in> \<real> \<Longrightarrow> Im (z / r) = Im z / Re r"
    1.22    by (metis Im_divide_of_real of_real_Re)
    1.23  
    1.24  lemma Re_sum[simp]: "Re (sum f s) = (\<Sum>x\<in>s. Re (f x))"
    1.25 @@ -691,6 +691,12 @@
    1.26  lemma in_Reals_norm: "z \<in> \<real> \<Longrightarrow> norm z = \<bar>Re z\<bar>"
    1.27    by (simp add: complex_is_Real_iff norm_complex_def)
    1.28  
    1.29 +lemma Re_Reals_divide: "r \<in> \<real> \<Longrightarrow> Re (r / z) = Re r * Re z / (norm z)\<^sup>2"
    1.30 +  by (simp add: Re_divide complex_is_Real_iff cmod_power2)
    1.31 +
    1.32 +lemma Im_Reals_divide: "r \<in> \<real> \<Longrightarrow> Im (r / z) = -Re r * Im z / (norm z)\<^sup>2"
    1.33 +  by (simp add: Im_divide complex_is_Real_iff cmod_power2)
    1.34 +
    1.35  lemma series_comparison_complex:
    1.36    fixes f:: "nat \<Rightarrow> 'a::banach"
    1.37    assumes sg: "summable g"