src/HOL/Analysis/Complex_Transcendental.thy
changeset 66480 4b8d1df8933b
parent 66466 aec5d9c88d69
child 66611 c375b64a6c24
     1.1 --- a/src/HOL/Analysis/Complex_Transcendental.thy	Mon Aug 21 19:20:02 2017 +0200
     1.2 +++ b/src/HOL/Analysis/Complex_Transcendental.thy	Mon Aug 21 20:49:15 2017 +0200
     1.3 @@ -73,6 +73,10 @@
     1.4  lemma holomorphic_on_exp [holomorphic_intros]: "exp holomorphic_on s"
     1.5    by (simp add: field_differentiable_within_exp holomorphic_on_def)
     1.6  
     1.7 +lemma holomorphic_on_exp' [holomorphic_intros]:
     1.8 +  "f holomorphic_on s \<Longrightarrow> (\<lambda>x. exp (f x)) holomorphic_on s"
     1.9 +  using holomorphic_on_compose[OF _ holomorphic_on_exp] by (simp add: o_def)
    1.10 +
    1.11  subsection\<open>Euler and de Moivre formulas.\<close>
    1.12  
    1.13  text\<open>The sine series times @{term i}\<close>