--- a/src/HOL/Analysis/Complex_Analysis_Basics.thy Mon Dec 04 23:10:52 2017 +0100
+++ b/src/HOL/Analysis/Complex_Analysis_Basics.thy Tue Dec 05 12:14:36 2017 +0100
@@ -367,6 +367,10 @@
"(\<And>i. i \<in> I \<Longrightarrow> (f i) holomorphic_on s) \<Longrightarrow> (\<lambda>x. sum (\<lambda>i. f i x) I) holomorphic_on s"
unfolding holomorphic_on_def by (metis field_differentiable_sum)
+lemma holomorphic_on_prod [holomorphic_intros]:
+ "(\<And>i. i \<in> I \<Longrightarrow> (f i) holomorphic_on s) \<Longrightarrow> (\<lambda>x. prod (\<lambda>i. f i x) I) holomorphic_on s"
+ by (induction I rule: infinite_finite_induct) (auto intro: holomorphic_intros)
+
lemma holomorphic_pochhammer [holomorphic_intros]:
"f holomorphic_on A \<Longrightarrow> (\<lambda>s. pochhammer (f s) n) holomorphic_on A"
by (induction n) (auto intro!: holomorphic_intros simp: pochhammer_Suc)