src/HOL/Analysis/Infinite_Products.thy
changeset 68616 cedf3480fdad
parent 68586 006da53a8ac1
child 68651 16d98ef49a2c
     1.1 --- a/src/HOL/Analysis/Infinite_Products.thy	Wed Jul 11 19:19:00 2018 +0100
     1.2 +++ b/src/HOL/Analysis/Infinite_Products.thy	Wed Jul 11 23:24:25 2018 +0100
     1.3 @@ -1762,6 +1762,12 @@
     1.4      by (simp add: add_eq_0_iff convergent_prod_iff_summable_complex)
     1.5  qed
     1.6  
     1.7 +lemma summable_Ln_complex:
     1.8 +  fixes z :: "nat \<Rightarrow> complex"
     1.9 +  assumes "convergent_prod z" "\<And>k. z k \<noteq> 0"
    1.10 +  shows "summable (\<lambda>k. Ln (z k))"
    1.11 +  using convergent_prod_def assms convergent_prod_iff_summable_complex by blast
    1.12 +
    1.13  
    1.14  subsection\<open>Embeddings from the reals into some complete real normed field\<close>
    1.15