# HG changeset patch
# User wenzelm
# Date 1646230129 -3600
# Node ID 74f0110bbd0a5c2c60e964cee39ec1c543bdcc5e
# Parent  ff60b4acd6ddf22d187162fa0cc79e72e49b7f72# Parent  e3388efdacd7d9b0aabaef9820e6d8b1e39c8b6b
merged

diff -r e3388efdacd7 -r 74f0110bbd0a src/HOL/Analysis/Complex_Analysis_Basics.thy
--- a/src/HOL/Analysis/Complex_Analysis_Basics.thy	Wed Mar 02 15:06:09 2022 +0100
+++ b/src/HOL/Analysis/Complex_Analysis_Basics.thy	Wed Mar 02 15:08:49 2022 +0100
@@ -532,6 +532,10 @@
   "(\<And>i. i \<in> I \<Longrightarrow> (f i) analytic_on S) \<Longrightarrow> (\<lambda>x. sum (\<lambda>i. f i x) I) analytic_on S"
   by (induct I rule: infinite_finite_induct) (auto simp: analytic_on_add)
 
+lemma analytic_on_prod [analytic_intros]:
+  "(\<And>i. i \<in> I \<Longrightarrow> (f i) analytic_on S) \<Longrightarrow> (\<lambda>x. prod (\<lambda>i. f i x) I) analytic_on S"
+  by (induct I rule: infinite_finite_induct) (auto simp: analytic_on_mult)
+
 lemma deriv_left_inverse:
   assumes "f holomorphic_on S" and "g holomorphic_on T"
       and "open S" and "open T"
diff -r e3388efdacd7 -r 74f0110bbd0a src/HOL/Complex_Analysis/Conformal_Mappings.thy
--- a/src/HOL/Complex_Analysis/Conformal_Mappings.thy	Wed Mar 02 15:06:09 2022 +0100
+++ b/src/HOL/Complex_Analysis/Conformal_Mappings.thy	Wed Mar 02 15:08:49 2022 +0100
@@ -114,6 +114,45 @@
     by blast
 qed
 
+lemma holomorphic_countable_zeros:
+  assumes S: "f holomorphic_on S" "open S" "connected S" and "fsigma S"
+      and "\<not> f constant_on S"
+    shows "countable {z\<in>S. f z = 0}"
+proof -
+  obtain F::"nat \<Rightarrow> complex set" 
+      where F: "range F \<subseteq> Collect compact" and Seq: "S = (\<Union>i. F i)"
+    using \<open>fsigma S\<close> by (meson fsigma_Union_compact)
+  have fin: "finite {z \<in> F i. f z = 0}" for i
+    using holomorphic_compact_finite_zeros assms F Seq Union_iff by blast
+  have "{z \<in> S. f z = 0} = (\<Union>i. {z \<in> F i. f z = 0})"
+    using Seq by auto
+  with fin show ?thesis
+    by (simp add: countable_finite)
+qed
+
+lemma holomorphic_countable_equal:
+  assumes "f holomorphic_on S" "g holomorphic_on S" "open S" "connected S" and "fsigma S"
+    and eq: "uncountable {z\<in>S. f z = g z}"
+  shows "S \<subseteq> {z\<in>S. f z = g z}"
+proof -
+  obtain z where z: "z\<in>S" "f z = g z"
+    using eq not_finite_existsD uncountable_infinite by blast
+  have "(\<lambda>x. f x - g x) holomorphic_on S"
+    by (simp add: assms holomorphic_on_diff)
+  then have "(\<lambda>x. f x - g x) constant_on S"
+    using holomorphic_countable_zeros assms by force
+  with z have "\<And>x. x\<in>S \<Longrightarrow> f x - g x = 0"
+    unfolding constant_on_def by force
+  then show ?thesis
+    by auto
+qed
+
+lemma holomorphic_countable_equal_UNIV:
+  assumes fg: "f holomorphic_on UNIV" "g holomorphic_on UNIV"
+    and eq: "uncountable {z. f z = g z}"
+  shows "f=g"
+  using holomorphic_countable_equal [OF fg] eq by fastforce
+
 subsection\<open>Open mapping theorem\<close>
 
 lemma holomorphic_contract_to_zero: