# HG changeset patch
# User Manuel Eberl <eberlm@in.tum.de>
# Date 1747856922 -7200
# Node ID 565545b7fe9d20a683fde5bcff1d82d09ab71506
# Parent  71f06e1f7fb4b3bff49472c4a28dc197b81ac1a2
three lemmas for HOL-Complex_Analysis, HOL-Computational_Algebra

diff -r 71f06e1f7fb4 -r 565545b7fe9d src/HOL/Complex_Analysis/Meromorphic.thy
--- a/src/HOL/Complex_Analysis/Meromorphic.thy	Wed May 21 20:13:43 2025 +0200
+++ b/src/HOL/Complex_Analysis/Meromorphic.thy	Wed May 21 21:48:42 2025 +0200
@@ -155,6 +155,21 @@
   by (intro is_pole_cong eventually_remove_sings_eq_at refl zorder_cong
             zor_poly_cong has_laurent_expansion_cong' tendsto_cong assms)+
 
+lemma remove_sings_has_laurent_expansion [laurent_expansion_intros]:
+  assumes "f has_laurent_expansion F"
+  shows   "remove_sings f has_laurent_expansion F"
+proof -
+  have "remove_sings f has_laurent_expansion F \<longleftrightarrow> f has_laurent_expansion F"
+  proof (rule has_laurent_expansion_cong)
+    have "isolated_singularity_at f 0"
+      using assms by (metis has_laurent_expansion_isolated_0)
+    thus "eventually (\<lambda>x. remove_sings f x = f x) (at 0)"
+      by (rule eventually_remove_sings_eq_at)
+  qed auto
+  with assms show ?thesis
+    by simp
+qed
+
 lemma get_all_poles_from_remove_sings:
   fixes f:: "complex \<Rightarrow> complex"
   defines "ff\<equiv>remove_sings f"
@@ -242,7 +257,7 @@
     using False remove_sings_eqI by auto
 qed simp
 
-lemma remove_sings_analytic_on:
+lemma remove_sings_analytic_at:
   assumes "isolated_singularity_at f z" "f \<midarrow>z\<rightarrow> c"
   shows   "remove_sings f analytic_on {z}"
 proof -
@@ -270,6 +285,24 @@
     using A(1,2) analytic_at by blast
 qed
 
+lemma remove_sings_analytic_on:
+  assumes "f analytic_on A"
+  shows   "remove_sings f analytic_on A"
+proof -
+  from assms obtain B where B: "open B" "A \<subseteq> B" "f holomorphic_on B"
+    by (metis analytic_on_holomorphic)
+  have "remove_sings f holomorphic_on B \<longleftrightarrow> f holomorphic_on B"
+  proof (rule holomorphic_cong)
+    fix z assume "z \<in> B"
+    have "f analytic_on {z}"
+      using \<open>z \<in> B\<close> B holomorphic_on_imp_analytic_at by blast
+    thus "remove_sings f z = f z"
+      by (rule remove_sings_at_analytic)
+  qed auto
+  thus ?thesis
+    using B analytic_on_holomorphic by blast
+qed
+
 lemma residue_remove_sings [simp]:
   assumes "isolated_singularity_at f z"
   shows   "residue (remove_sings f) z = residue f z"
@@ -1585,7 +1618,7 @@
   from assms(1) have "f \<midarrow>z\<rightarrow> 0"
     by (simp add: isolated_zero_def)
   with assms(2) have "remove_sings f analytic_on {z}"
-    by (intro remove_sings_analytic_on)
+    by (intro remove_sings_analytic_at)
   hence "zorder (remove_sings f) z > 0"
     using assms by (intro zorder_isolated_zero_pos) auto
   thus ?thesis
@@ -1714,7 +1747,7 @@
   shows   "zorder f z = 0"
 proof -
   have "remove_sings f analytic_on {z}"
-    using assms meromorphic_at_iff not_essential_def remove_sings_analytic_on by blast
+    using assms meromorphic_at_iff not_essential_def remove_sings_analytic_at by blast
   moreover from this and assms have "remove_sings f z \<noteq> 0"
     using isolated_zero_def meromorphic_at_iff non_zero_neighbour remove_sings_eq_0_iff by blast
   moreover have "frequently (\<lambda>z. remove_sings f z \<noteq> 0) (at z)"
diff -r 71f06e1f7fb4 -r 565545b7fe9d src/HOL/Computational_Algebra/Polynomial.thy
--- a/src/HOL/Computational_Algebra/Polynomial.thy	Wed May 21 20:13:43 2025 +0200
+++ b/src/HOL/Computational_Algebra/Polynomial.thy	Wed May 21 21:48:42 2025 +0200
@@ -2042,6 +2042,42 @@
   ultimately show False by linarith
 qed
 
+lemma poly_eqI_degree_lead_coeff:
+  fixes p q :: "'a :: {comm_ring_1, ring_no_zero_divisors} poly"
+  assumes "poly.coeff p n = poly.coeff q n" "card A \<ge> n" "degree p \<le> n" "degree q \<le> n"
+  assumes "\<And>z. z \<in> A \<Longrightarrow> poly p z = poly q z"
+  shows   "p = q"
+proof (rule ccontr)
+  assume "p \<noteq> q"
+
+  have "n > 0"
+  proof (rule ccontr)
+    assume "\<not>(n > 0)"
+    thus False
+      using assms \<open>p \<noteq> q\<close> by (auto elim!: degree_eq_zeroE)
+  qed
+
+  have "n \<le> card A"
+    by fact
+  also have "card A \<le> card {x. poly (p - q) x = 0}"
+    by (intro card_mono poly_roots_finite) (use \<open>p \<noteq> q\<close> assms in auto)
+  also have "card {x. poly (p - q) x = 0} \<le> degree (p - q)"
+    by (rule card_poly_roots_bound) (use \<open>p \<noteq> q\<close> in auto)
+  also have "degree (p - q) < n"
+  proof (intro degree_lessI allI impI)
+    fix k assume "k \<ge> n"
+    show "poly.coeff (p - q) k = 0"
+    proof (cases "k = n")
+      case False
+      hence "poly.coeff p k = 0" "poly.coeff q k = 0"
+        using assms \<open>k \<ge> n\<close> by (auto simp: coeff_eq_0)
+      thus ?thesis
+        by simp
+    qed (use assms in auto)
+  qed (use \<open>n > 0\<close> in auto)
+  finally show False
+    by simp
+qed
 
 
 subsubsection \<open>Order of polynomial roots\<close>