# HG changeset patch
# User Manuel Eberl <manuel@pruvisto.org>
# Date 1744966696 -7200
# Node ID ff4b062aae573d061e92a4a24c35f4929c31d9c7
# Parent  3704717ed7bf986256f1685a4c4f732cf6a2299c
moved some lemmas to where they fit better

diff -r 3704717ed7bf -r ff4b062aae57 src/HOL/Analysis/Derivative.thy
--- a/src/HOL/Analysis/Derivative.thy	Mon Apr 21 08:24:58 2025 +0200
+++ b/src/HOL/Analysis/Derivative.thy	Fri Apr 18 10:58:16 2025 +0200
@@ -1742,7 +1742,7 @@
         using islimpt_approachable_real[of x S] not_bot
         by (auto simp add: trivial_limit_within)
       then show ?thesis
-        using eq_iff_diff_eq_0 by fastforce
+        using eq_iff_diff_eq_0 by (metis add.commute diff_add_cancel)
     qed
   qed (use f' f'' in \<open>auto simp: has_vector_derivative_def\<close>)
   then show ?thesis
@@ -1777,6 +1777,17 @@
   by (intro vector_derivative_unique_within[OF not_bot vector_derivative_works[THEN iffD1] y])
      (auto simp: differentiable_def has_vector_derivative_def)
 
+lemma vector_derivative_translate [simp]:
+  "vector_derivative ((+) z \<circ> g) (at x within A) = vector_derivative g (at x within A)"
+proof -
+  have "(((+) z \<circ> g) has_vector_derivative g') (at x within A)"
+    if "(g has_vector_derivative g') (at x within A)" for g :: "real \<Rightarrow> 'a" and z g'
+    unfolding o_def using that by (auto intro!: derivative_eq_intros)
+  from this[of g _ z] this[of "\<lambda>x. z + g x" _ "-z"] show ?thesis
+    unfolding vector_derivative_def
+    by (intro arg_cong[where f = Eps] ext) (auto simp: o_def algebra_simps)
+qed
+
 lemma deriv_of_real [simp]: 
   "at x within A \<noteq> bot \<Longrightarrow> vector_derivative of_real (at x within A) = 1"
   by (auto intro!: vector_derivative_within derivative_eq_intros)
@@ -2256,6 +2267,43 @@
 definition\<^marker>\<open>tag important\<close> deriv :: "('a \<Rightarrow> 'a::real_normed_field) \<Rightarrow> 'a \<Rightarrow> 'a" where
   "deriv f x \<equiv> SOME D. DERIV f x :> D"
 
+lemma deriv_shift_0: "deriv f z = deriv (f \<circ> (\<lambda>x. z + x)) 0"
+proof -
+  have *: "(f \<circ> (+) z has_field_derivative D) (at z')"
+    if "(f has_field_derivative D) (at (z + z'))" for D z z' and f :: "'a \<Rightarrow> 'a"
+  proof -
+    have "(f \<circ> (+) z has_field_derivative D * 1) (at z')"
+      by (rule DERIV_chain that derivative_eq_intros refl)+ auto
+    thus ?thesis by simp
+  qed
+  have "(\<lambda>D. (f has_field_derivative D) (at z)) = (\<lambda> D. (f \<circ> (+) z has_field_derivative D) (at 0))"
+    using *[of f _ z 0] *[of "f \<circ> (+) z" _ "-z" z] by (intro ext iffI) (auto simp: o_def)
+  thus ?thesis
+    by (simp add: deriv_def)
+qed
+
+lemma deriv_shift_0': "NO_MATCH 0 z \<Longrightarrow> deriv f z = deriv (f \<circ> (\<lambda>x. z + x)) 0"
+  by (rule deriv_shift_0)
+
+lemma higher_deriv_shift_0: "(deriv ^^ n) f z = (deriv ^^ n) (f \<circ> (\<lambda>x. z + x)) 0"
+proof (induction n arbitrary: f)
+  case (Suc n)
+  have "(deriv ^^ Suc n) f z = (deriv ^^ n) (deriv f) z"
+    by (subst funpow_Suc_right) auto
+  also have "\<dots> = (deriv ^^ n) (\<lambda>x. deriv f (z + x)) 0"
+    by (subst Suc) (auto simp: o_def)
+  also have "\<dots> = (deriv ^^ n) (\<lambda>x. deriv (\<lambda>xa. f (z + x + xa)) 0) 0"
+    by (subst deriv_shift_0) (auto simp: o_def)
+  also have "(\<lambda>x. deriv (\<lambda>xa. f (z + x + xa)) 0) = deriv (\<lambda>x. f (z + x))"
+    by (rule ext) (simp add: deriv_shift_0' o_def add_ac)
+  also have "(deriv ^^ n) \<dots> 0 = (deriv ^^ Suc n) (f \<circ> (\<lambda>x. z + x)) 0"
+    by (subst funpow_Suc_right) (auto simp: o_def)
+  finally show ?case .
+qed auto
+
+lemma higher_deriv_shift_0': "NO_MATCH 0 z \<Longrightarrow> (deriv ^^ n) f z = (deriv ^^ n) (f \<circ> (\<lambda>x. z + x)) 0"
+  by (rule higher_deriv_shift_0)
+
 lemma DERIV_imp_deriv: "DERIV f x :> f' \<Longrightarrow> deriv f x = f'"
   unfolding deriv_def by (metis some_equality DERIV_unique)
 
diff -r 3704717ed7bf -r ff4b062aae57 src/HOL/Analysis/FPS_Convergence.thy
--- a/src/HOL/Analysis/FPS_Convergence.thy	Mon Apr 21 08:24:58 2025 +0200
+++ b/src/HOL/Analysis/FPS_Convergence.thy	Fri Apr 18 10:58:16 2025 +0200
@@ -61,6 +61,9 @@
 lemma open_eball [simp, intro]: "open (eball z r)" 
   by (cases r) auto
 
+lemma connected_eball [intro]: "connected (eball (z :: 'a :: real_normed_vector) r)"
+  by (cases r) auto
+
 
 subsection \<open>Basic properties of convergent power series\<close>
 
diff -r 3704717ed7bf -r ff4b062aae57 src/HOL/Analysis/Infinite_Products.thy
--- a/src/HOL/Analysis/Infinite_Products.thy	Mon Apr 21 08:24:58 2025 +0200
+++ b/src/HOL/Analysis/Infinite_Products.thy	Fri Apr 18 10:58:16 2025 +0200
@@ -846,11 +846,16 @@
       by (metis convergent_mult_const_iff \<open>C \<noteq> 0\<close> cong cf convergent_LIMSEQ_iff convergent_prod_iff_convergent convergent_prod_imp_convergent g)
   next
     assume cg: "convergent_prod g"
-    have "\<exists>a. C * a \<noteq> 0 \<and> (\<lambda>n. prod g {..n}) \<longlonglongrightarrow> a"
-      by (metis (no_types) \<open>C \<noteq> 0\<close> cg convergent_prod_iff_nz_lim divide_eq_0_iff g nonzero_mult_div_cancel_right)
+    have **: "eventually (\<lambda>n. prod g {..n} = prod f {..n} / C) sequentially"
+      using * by eventually_elim (use \<open>C \<noteq> 0\<close> in auto)
+    from cg and g have "\<not> (\<lambda>n. prod g {..n}) \<longlonglongrightarrow> 0"
+      by simp
+    then have "\<not> (\<lambda>n. prod f {..n}) \<longlonglongrightarrow> 0"
+      using ** \<open>C \<noteq> 0\<close> filterlim_cong by fastforce
     then show "convergent_prod f"
-      using "*" tendsto_mult_left filterlim_cong
-      by (fastforce simp add: convergent_prod_iff_nz_lim f)
+      by (metis \<open>C \<noteq> 0\<close> cg convergent_LIMSEQ_iff
+          convergent_mult_const_iff convergent_prod_iff_convergent
+          convergent_prod_imp_convergent f local.cong)
   qed
 qed
 
@@ -953,8 +958,14 @@
 
 lemma convergent_prod_If_finite[simp, intro]:
   fixes f :: "nat \<Rightarrow> 'a::{idom,t2_space}"
-  shows "finite {r. P r} \<Longrightarrow> convergent_prod (\<lambda>r. if P r then f r else 1)"
-  using convergent_prod_def has_prod_If_finite has_prod_def by fastforce
+  assumes "finite {r. P r}"
+  shows   "convergent_prod (\<lambda>r. if P r then f r else 1)"
+proof -
+  have "(\<lambda>r. if P r then f r else 1) has_prod (\<Prod>r | P r. f r)"
+    by (rule has_prod_If_finite) fact
+  thus ?thesis
+    by (meson convergent_prod_def has_prod_def)
+qed
 
 lemma has_prod_single:
   fixes f :: "nat \<Rightarrow> 'a::{idom,t2_space}"
diff -r 3704717ed7bf -r ff4b062aae57 src/HOL/Analysis/Infinite_Sum.thy
--- a/src/HOL/Analysis/Infinite_Sum.thy	Mon Apr 21 08:24:58 2025 +0200
+++ b/src/HOL/Analysis/Infinite_Sum.thy	Fri Apr 18 10:58:16 2025 +0200
@@ -27,6 +27,7 @@
     Elementary_Topology
     "HOL-Library.Extended_Nonnegative_Real"
     "HOL-Library.Complex_Order"
+    "HOL-Computational_Algebra.Formal_Power_Series"
 begin
 
 subsection \<open>Definition and syntax\<close>
@@ -3578,5 +3579,79 @@
   shows "(f has_sum S) A \<Longrightarrow> ((\<lambda>x. -f x) has_sum (-S)) A"
   using has_sum_cmult_right[of f A S "-1"] by simp
 
+
+subsection \<open>Infinite sums of formal power series\<close>
+
+text \<open>
+  Consequently, a family $(f_x)_{x\in A}$ of formal power series sums to a series $s$ iff for
+  any $n\geq 0$, the set $A_n = \{x\in A \mid [X^n]\,f_x \neq 0\}$ is finite and
+  $[X^n]\,s = \sum_{x\in A_n} [X^n]\,f_x$.
+
+  The first condition can be rephrased as follows: for any $n\geq 0$, for all but finitely many
+  $x$, the series $f_x$ has subdegree ${>}\,n$.
+\<close>
+lemma has_sum_fpsI:
+  assumes "\<And>n. finite {x\<in>A. fps_nth (F x) n \<noteq> 0}"
+  assumes "\<And>n. fps_nth S n = (\<Sum>x | x \<in> A \<and> fps_nth (F x) n \<noteq> 0. fps_nth (F x) n)"
+  shows   "(F has_sum S) A"
+  unfolding has_sum_def
+proof (rule tendsto_fpsI)
+  fix n :: nat
+  define B where "B = {x\<in>A. fps_nth (F x) n \<noteq> 0}"
+  from assms(1) have [intro]: "finite B"
+    unfolding B_def by auto
+  moreover have "B \<subseteq> A"
+    by (auto simp: B_def)
+  ultimately have "eventually (\<lambda>X. finite X \<and> B \<subseteq> X \<and> X \<subseteq> A) (finite_subsets_at_top A)"
+    by (subst eventually_finite_subsets_at_top) blast
+  thus "eventually (\<lambda>X. fps_nth (\<Sum>x\<in>X. F x) n = fps_nth S n) (finite_subsets_at_top A)"
+  proof eventually_elim
+    case (elim X)
+    have "fps_nth (\<Sum>x\<in>X. F x) n = (\<Sum>x\<in>X. fps_nth (F x) n)"
+      by (simp add: fps_sum_nth)
+    also have "\<dots> = (\<Sum>x\<in>B. fps_nth (F x) n)"
+      by (rule sum.mono_neutral_right)  (use \<open>finite B\<close> \<open>B \<subseteq> A\<close> elim in \<open>auto simp: B_def\<close>)
+    also have "\<dots> = fps_nth S n"
+      using assms(2)[of n] by (simp add: B_def)
+    finally show "fps_nth (\<Sum>x\<in>X. F x) n = fps_nth S n" .
+  qed
+qed
+
+lemma has_sum_fpsD:
+  fixes F :: "'a \<Rightarrow> 'b :: ab_group_add fps"
+  assumes "(F has_sum S) A"
+  shows   "finite {x\<in>A. fps_nth (F x) n \<noteq> 0}"
+          "fps_nth S n = (\<Sum>x | x \<in> A \<and> fps_nth (F x) n \<noteq> 0. fps_nth (F x) n)"
+proof -
+  from assms have "\<forall>\<^sub>F X in finite_subsets_at_top A. fps_nth (sum F X) k = fps_nth S k" for k
+    unfolding has_sum_def tendsto_fps_iff by blast
+  hence "\<forall>\<^sub>F X in finite_subsets_at_top A. fps_nth (sum F X) n = fps_nth S n"
+    by eventually_elim force
+  then obtain B where [intro, simp]: "finite B" and B: "B \<subseteq> A"
+     "\<And>X. finite X \<Longrightarrow> B \<subseteq> X \<Longrightarrow> X \<subseteq> A \<Longrightarrow> fps_nth (sum F X) n = fps_nth S n"
+    unfolding eventually_finite_subsets_at_top by metis
+
+  have subset: "{x\<in>A. fps_nth (F x) n \<noteq> 0} \<subseteq> B"
+  proof safe
+    fix x assume x: "x \<in> A" "fps_nth (F x) n \<noteq> 0"
+    have "fps_nth (sum F B) n = fps_nth S n"
+      by (rule B(2)) (use B(1) in auto)
+    moreover have "fps_nth (sum F (insert x B)) n = fps_nth S n"
+      by (rule B(2)) (use B(1) x in auto)
+    ultimately show "x \<in> B"
+      using x by (auto simp: sum.insert_if split: if_splits)
+  qed
+  thus finite: "finite {x\<in>A. fps_nth (F x) n \<noteq> 0}"
+    by (rule finite_subset) auto
+
+  have "fps_nth S n = fps_nth (\<Sum>x\<in>B. F x) n"
+    by (rule sym, rule B(2)) (use B(1) in auto)
+  also have "\<dots> = (\<Sum>x\<in>B. fps_nth (F x) n)"
+    by (simp add: fps_sum_nth)
+  also have "\<dots> = (\<Sum>x | x \<in> A \<and> fps_nth (F x) n \<noteq> 0. fps_nth (F x) n)"
+    by (rule sum.mono_neutral_right) (use subset B(1) in auto)
+  finally show "fps_nth S n = (\<Sum>x | x \<in> A \<and> fps_nth (F x) n \<noteq> 0. fps_nth (F x) n)" .
+qed
+
 end
 
diff -r 3704717ed7bf -r ff4b062aae57 src/HOL/Complex_Analysis/Complex_Residues.thy
--- a/src/HOL/Complex_Analysis/Complex_Residues.thy	Mon Apr 21 08:24:58 2025 +0200
+++ b/src/HOL/Complex_Analysis/Complex_Residues.thy	Fri Apr 18 10:58:16 2025 +0200
@@ -52,6 +52,26 @@
   with assms show ?thesis by simp
 qed
 
+lemma residue_shift_0: "residue f z = residue (\<lambda>x. f (z + x)) 0"
+proof -
+  define Q where
+    "Q = (\<lambda>r f z \<epsilon>. (f has_contour_integral complex_of_real (2 * pi) * \<i> * r) (circlepath z \<epsilon>))"
+  define P where
+    "P = (\<lambda>r f z. \<exists>e>0. \<forall>\<epsilon>>0. \<epsilon> < e \<longrightarrow> Q r f z \<epsilon>)"
+  have path_eq: "circlepath (z - w) \<epsilon> = (+) (-w) \<circ> circlepath z \<epsilon>" for z w \<epsilon>
+    by (simp add: circlepath_def o_def part_circlepath_def algebra_simps)
+  have *: "P r f z" if "P r (\<lambda>x. f (x + w)) (z - w)" for r w f z
+    using that by (auto simp: P_def Q_def path_eq has_contour_integral_translate)
+  have "(SOME r. P r f z) = (SOME r. P r (\<lambda>x. f (z + x)) 0)"
+    using *[of _ f z z] *[of _ "\<lambda>x. f (z + x)" "-z"]
+    by (intro arg_cong[where f = Eps] ext iffI) (simp_all add: add_ac)
+  thus ?thesis
+    by (simp add: residue_def P_def Q_def)
+qed
+
+lemma residue_shift_0': "NO_MATCH 0 z \<Longrightarrow> residue f z = residue (\<lambda>x. f (z + x)) 0"
+  by (rule residue_shift_0)
+
 lemma contour_integral_circlepath_eq:
   assumes "open s" and f_holo:"f holomorphic_on (s-{z})" and "0<e1" "e1\<le>e2"
     and e2_cball:"cball z e2 \<subseteq> s"
diff -r 3704717ed7bf -r ff4b062aae57 src/HOL/Complex_Analysis/Contour_Integration.thy
--- a/src/HOL/Complex_Analysis/Contour_Integration.thy	Mon Apr 21 08:24:58 2025 +0200
+++ b/src/HOL/Complex_Analysis/Contour_Integration.thy	Fri Apr 18 10:58:16 2025 +0200
@@ -68,6 +68,18 @@
   using has_integral_unique
   by (auto simp: has_contour_integral_def)
 
+lemma has_contour_integral_translate:
+  "(f has_contour_integral I) ((+) z \<circ> g) \<longleftrightarrow> ((\<lambda>x. f (x + z)) has_contour_integral I) g"
+  by (simp add: has_contour_integral_def add_ac)
+
+lemma contour_integrable_translate:
+  "f contour_integrable_on ((+) z \<circ> g) \<longleftrightarrow> (\<lambda>x. f (x + z)) contour_integrable_on g"
+  by (simp add: contour_integrable_on_def has_contour_integral_translate)
+
+lemma contour_integral_translate:
+  "contour_integral ((+) z \<circ> g) f = contour_integral g (\<lambda>x. f (x + z))"
+  by (simp add: contour_integral_def contour_integrable_translate has_contour_integral_translate)
+
 lemma has_contour_integral_integrable: "(f has_contour_integral i) g \<Longrightarrow> f contour_integrable_on g"
   using contour_integrable_on_def by blast
 
diff -r 3704717ed7bf -r ff4b062aae57 src/HOL/Complex_Analysis/Laurent_Convergence.thy
--- a/src/HOL/Complex_Analysis/Laurent_Convergence.thy	Mon Apr 21 08:24:58 2025 +0200
+++ b/src/HOL/Complex_Analysis/Laurent_Convergence.thy	Fri Apr 18 10:58:16 2025 +0200
@@ -4,80 +4,6 @@
 
 begin
 
-instance fps :: (semiring_char_0) semiring_char_0
-proof
-  show "inj (of_nat :: nat \<Rightarrow> 'a fps)"
-  proof
-    fix m n :: nat
-    assume "of_nat m = (of_nat n :: 'a fps)"
-    hence "fps_nth (of_nat m) 0 = (fps_nth (of_nat n) 0 :: 'a)"
-      by (simp only: )
-    thus "m = n"
-      by simp
-  qed
-qed
-
-instance fls :: (semiring_char_0) semiring_char_0
-proof
-  show "inj (of_nat :: nat \<Rightarrow> 'a fls)"
-    by (metis fls_regpart_of_nat injI of_nat_eq_iff)
-qed
-
-lemma fls_const_eq_0_iff [simp]: "fls_const c = 0 \<longleftrightarrow> c = 0"
-  using fls_const_0 fls_const_nonzero by blast
-
-lemma fls_subdegree_add_eq1:
-  assumes "f \<noteq> 0" "fls_subdegree f < fls_subdegree g"
-  shows   "fls_subdegree (f + g) = fls_subdegree f"
-proof (intro antisym)
-  from assms have *: "fls_nth (f + g) (fls_subdegree f) \<noteq> 0"
-    by auto
-  from * show "fls_subdegree (f + g) \<le> fls_subdegree f"
-    by (rule fls_subdegree_leI)
-  from * have "f + g \<noteq> 0"
-    using fls_nonzeroI by blast
-  thus "fls_subdegree f \<le> fls_subdegree (f + g)"
-    using assms(2) fls_plus_subdegree by force
-qed
-
-lemma fls_subdegree_add_eq2:
-  assumes "g \<noteq> 0" "fls_subdegree g < fls_subdegree f"
-  shows   "fls_subdegree (f + g) = fls_subdegree g"
-proof (intro antisym)
-  from assms have *: "fls_nth (f + g) (fls_subdegree g) \<noteq> 0"
-    by auto
-  from * show "fls_subdegree (f + g) \<le> fls_subdegree g"
-    by (rule fls_subdegree_leI)
-  from * have "f + g \<noteq> 0"
-    using fls_nonzeroI by blast
-  thus "fls_subdegree g \<le> fls_subdegree (f + g)"
-    using assms(2) fls_plus_subdegree by force
-qed
-
-lemma fls_subdegree_diff_eq1:
-  assumes "f \<noteq> 0" "fls_subdegree f < fls_subdegree g"
-  shows   "fls_subdegree (f - g) = fls_subdegree f"
-  using fls_subdegree_add_eq1[of f "-g"] assms by simp
-
-lemma fls_subdegree_diff_eq2:
-  assumes "g \<noteq> 0" "fls_subdegree g < fls_subdegree f"
-  shows   "fls_subdegree (f - g) = fls_subdegree g"
-  using fls_subdegree_add_eq2[of "-g" f] assms by simp
-
-lemma nat_minus_fls_subdegree_plus_const_eq:
-  "nat (-fls_subdegree (F + fls_const c)) = nat (-fls_subdegree F)"
-proof (cases "fls_subdegree F < 0")
-  case True
-  hence "fls_subdegree (F + fls_const c) = fls_subdegree F"
-    by (intro fls_subdegree_add_eq1) auto
-  thus ?thesis
-    by simp
-next
-  case False
-  thus ?thesis
-    by (auto simp: fls_subdegree_ge0I)
-qed
-
 
 definition%important fls_conv_radius :: "complex fls \<Rightarrow> ereal" where
   "fls_conv_radius f = fps_conv_radius (fls_regpart f)"
@@ -139,12 +65,6 @@
   and eval_fps_of_int [simp]: "eval_fps (of_int m) z = of_int m"
   by (simp_all flip: fps_of_nat fps_of_int)
 
-lemma fls_subdegree_numeral [simp]: "fls_subdegree (numeral n) = 0"
-  by (metis fls_subdegree_of_nat of_nat_numeral)
-
-lemma fls_regpart_numeral [simp]: "fls_regpart (numeral n) = numeral n"
-  by (metis fls_regpart_of_nat of_nat_numeral)
-
 lemma fps_conv_radius_of_nat [simp]: "fps_conv_radius (of_nat n) = \<infinity>"
   and fps_conv_radius_of_int [simp]: "fps_conv_radius (of_int m) = \<infinity>"
   by (simp_all flip: fps_of_nat fps_of_int)
@@ -486,9 +406,6 @@
 lemmas has_field_derivative_eval_fps' [derivative_intros] =
   DERIV_chain2[OF has_field_derivative_eval_fps]
 
-lemma fps_deriv_fls_regpart: "fps_deriv (fls_regpart F) = fls_regpart (fls_deriv F)"
-  by (intro fps_ext) (auto simp: add_ac)
-
 (* TODO: generalise for nonneg subdegree *)
 lemma has_field_derivative_eval_fls:
   assumes "z \<in> eball 0 (fls_conv_radius f) - {0}"
@@ -1186,43 +1103,6 @@
   shows   "f has_fps_expansion fps_expansion f 0"
   using assms has_fps_expansion_fps_expansion analytic_at by fast
 
-lemma deriv_shift_0: "deriv f z = deriv (f \<circ> (\<lambda>x. z + x)) 0"
-proof -
-  have *: "(f \<circ> (+) z has_field_derivative D) (at z')"
-    if "(f has_field_derivative D) (at (z + z'))" for D z z' and f :: "'a \<Rightarrow> 'a"
-  proof -
-    have "(f \<circ> (+) z has_field_derivative D * 1) (at z')"
-      by (rule DERIV_chain that derivative_eq_intros refl)+ auto
-    thus ?thesis by simp
-  qed
-  have "(\<lambda>D. (f has_field_derivative D) (at z)) = (\<lambda> D. (f \<circ> (+) z has_field_derivative D) (at 0))"
-    using *[of f _ z 0] *[of "f \<circ> (+) z" _ "-z" z] by (intro ext iffI) (auto simp: o_def)
-  thus ?thesis
-    by (simp add: deriv_def)
-qed
-
-lemma deriv_shift_0': "NO_MATCH 0 z \<Longrightarrow> deriv f z = deriv (f \<circ> (\<lambda>x. z + x)) 0"
-  by (rule deriv_shift_0)
-
-lemma higher_deriv_shift_0: "(deriv ^^ n) f z = (deriv ^^ n) (f \<circ> (\<lambda>x. z + x)) 0"
-proof (induction n arbitrary: f)
-  case (Suc n)
-  have "(deriv ^^ Suc n) f z = (deriv ^^ n) (deriv f) z"
-    by (subst funpow_Suc_right) auto
-  also have "\<dots> = (deriv ^^ n) (\<lambda>x. deriv f (z + x)) 0"
-    by (subst Suc) (auto simp: o_def)
-  also have "\<dots> = (deriv ^^ n) (\<lambda>x. deriv (\<lambda>xa. f (z + x + xa)) 0) 0"
-    by (subst deriv_shift_0) (auto simp: o_def)
-  also have "(\<lambda>x. deriv (\<lambda>xa. f (z + x + xa)) 0) = deriv (\<lambda>x. f (z + x))"
-    by (rule ext) (simp add: deriv_shift_0' o_def add_ac)
-  also have "(deriv ^^ n) \<dots> 0 = (deriv ^^ Suc n) (f \<circ> (\<lambda>x. z + x)) 0"
-    by (subst funpow_Suc_right) (auto simp: o_def)
-  finally show ?case .
-qed auto
-
-lemma higher_deriv_shift_0': "NO_MATCH 0 z \<Longrightarrow> (deriv ^^ n) f z = (deriv ^^ n) (f \<circ> (\<lambda>x. z + x)) 0"
-  by (rule higher_deriv_shift_0)
-
 lemma analytic_at_imp_has_fps_expansion:
   assumes "f analytic_on {z}"
   shows   "(\<lambda>x. f (z + x)) has_fps_expansion fps_expansion f z"
@@ -1624,49 +1504,6 @@
     by (simp add: field_simps)
 qed
 
-lemma vector_derivative_translate [simp]:
-  "vector_derivative ((+) z \<circ> g) (at x within A) = vector_derivative g (at x within A)"
-proof -
-  have "(((+) z \<circ> g) has_vector_derivative g') (at x within A)"
-    if "(g has_vector_derivative g') (at x within A)" for g :: "real \<Rightarrow> 'a" and z g'
-    unfolding o_def using that by (auto intro!: derivative_eq_intros)
-  from this[of g _ z] this[of "\<lambda>x. z + g x" _ "-z"] show ?thesis
-    unfolding vector_derivative_def
-    by (intro arg_cong[where f = Eps] ext) (auto simp: o_def algebra_simps)
-qed
-
-lemma has_contour_integral_translate:
-  "(f has_contour_integral I) ((+) z \<circ> g) \<longleftrightarrow> ((\<lambda>x. f (x + z)) has_contour_integral I) g"
-  by (simp add: has_contour_integral_def add_ac)
-
-lemma contour_integrable_translate:
-  "f contour_integrable_on ((+) z \<circ> g) \<longleftrightarrow> (\<lambda>x. f (x + z)) contour_integrable_on g"
-  by (simp add: contour_integrable_on_def has_contour_integral_translate)
-
-lemma contour_integral_translate:
-  "contour_integral ((+) z \<circ> g) f = contour_integral g (\<lambda>x. f (x + z))"
-  by (simp add: contour_integral_def contour_integrable_translate has_contour_integral_translate)
-
-lemma residue_shift_0: "residue f z = residue (\<lambda>x. f (z + x)) 0"
-proof -
-  define Q where
-    "Q = (\<lambda>r f z \<epsilon>. (f has_contour_integral complex_of_real (2 * pi) * \<i> * r) (circlepath z \<epsilon>))"
-  define P where
-    "P = (\<lambda>r f z. \<exists>e>0. \<forall>\<epsilon>>0. \<epsilon> < e \<longrightarrow> Q r f z \<epsilon>)"
-  have path_eq: "circlepath (z - w) \<epsilon> = (+) (-w) \<circ> circlepath z \<epsilon>" for z w \<epsilon>
-    by (simp add: circlepath_def o_def part_circlepath_def algebra_simps)
-  have *: "P r f z" if "P r (\<lambda>x. f (x + w)) (z - w)" for r w f z
-    using that by (auto simp: P_def Q_def path_eq has_contour_integral_translate)
-  have "(SOME r. P r f z) = (SOME r. P r (\<lambda>x. f (z + x)) 0)"
-    using *[of _ f z z] *[of _ "\<lambda>x. f (z + x)" "-z"]
-    by (intro arg_cong[where f = Eps] ext iffI) (simp_all add: add_ac)
-  thus ?thesis
-    by (simp add: residue_def P_def Q_def)
-qed
-
-lemma residue_shift_0': "NO_MATCH 0 z \<Longrightarrow> residue f z = residue (\<lambda>x. f (z + x)) 0"
-  by (rule residue_shift_0)
-
 lemma has_laurent_expansion_residue_0:
   assumes "f has_laurent_expansion F"
   shows   "residue f 0 = fls_residue F"
@@ -1768,9 +1605,6 @@
     by (simp add: fls_conv_radius_altdef G_def)
 qed
 
-lemma connected_eball [intro]: "connected (eball (z :: 'a :: real_normed_vector) r)"
-  by (cases r) auto
-
 lemma eval_fls_eqI:
   assumes "f has_laurent_expansion F" "f holomorphic_on eball 0 r - {0}"
   assumes "z \<in> eball 0 r - {0}"
@@ -1821,7 +1655,7 @@
 
 lemma tendsto_0_subdegree_iff_0:
   assumes F:"f has_laurent_expansion F" and "F\<noteq>0"
-  shows "(f \<midarrow>0\<rightarrow>0) \<longleftrightarrow> fls_subdegree F > 0"
+  shows "(f \<midarrow>0\<rightarrow> 0) \<longleftrightarrow> fls_subdegree F > 0"
 proof -
   have ?thesis if "is_pole f 0"
   proof -
@@ -1872,15 +1706,15 @@
 qed
 
 lemma tendsto_0_subdegree_iff:
-  assumes F:"(\<lambda>w. f (z+w)) has_laurent_expansion F" and "F\<noteq>0"
-  shows "(f \<midarrow>z\<rightarrow>0) \<longleftrightarrow> fls_subdegree F > 0"
+  assumes F: "(\<lambda>w. f (z+w)) has_laurent_expansion F" and "F \<noteq> 0"
+  shows "(f \<midarrow>z\<rightarrow> 0) \<longleftrightarrow> fls_subdegree F > 0"
   apply (subst Lim_at_zero)
   apply (rule tendsto_0_subdegree_iff_0)
   using assms by auto
 
 lemma is_pole_0_deriv_divide_iff:
-  assumes F:"f has_laurent_expansion F" and "F\<noteq>0"
-  shows "is_pole (\<lambda>x. deriv f x / f x) 0 \<longleftrightarrow> is_pole f 0 \<or> (f \<midarrow>0\<rightarrow>0)"
+  assumes F: "f has_laurent_expansion F" and "F \<noteq> 0"
+  shows "is_pole (\<lambda>x. deriv f x / f x) 0 \<longleftrightarrow> is_pole f 0 \<or> (f \<midarrow>0\<rightarrow> 0)"
 proof -
   have "(\<lambda>x. deriv f x / f x) has_laurent_expansion fls_deriv F / F"
     using F by (auto intro:laurent_expansion_intros)
@@ -2396,43 +2230,6 @@
   qed
 qed
 
-lemma subdegree_fps_compose [simp]:
-  fixes F G :: "'a :: idom fps"
-  assumes [simp]: "fps_nth G 0 = 0"
-  shows "subdegree (fps_compose F G) = subdegree F * subdegree G"
-proof (cases "G = 0"; cases "F = 0")
-  assume [simp]: "G \<noteq> 0" "F \<noteq> 0"
-  define m where "m = subdegree F"
-  define F' where "F' = fps_shift m F"
-  have F_eq: "F = F' * fps_X ^ m"
-    unfolding F'_def by (simp add: fps_shift_times_fps_X_power m_def)
-  have [simp]: "F' \<noteq> 0"
-    using \<open>F \<noteq> 0\<close> unfolding F_eq by auto
-  have "subdegree (fps_compose F G) = subdegree (fps_compose F' G) + m * subdegree G"
-    by (simp add: F_eq fps_compose_mult_distrib fps_compose_eq_0_iff flip: fps_compose_power)
-  also have "subdegree (fps_compose F' G) = 0"
-    by (intro subdegree_eq_0) (auto simp: F'_def m_def)
-  finally show ?thesis by (simp add: m_def)
-qed auto
-
-lemma fls_subdegree_power_int [simp]:
-  fixes   F :: "'a :: field fls"
-  shows "fls_subdegree (F powi n) = n * fls_subdegree F"
-  by (auto simp: power_int_def fls_subdegree_pow)
-
-lemma subdegree_fls_compose_fps [simp]:
-  fixes G :: "'a :: field fps"
-  assumes [simp]: "fps_nth G 0 = 0"
-  shows "fls_subdegree (fls_compose_fps F G) = fls_subdegree F * subdegree G"
-proof (cases "F = 0"; cases "G = 0")
-  assume [simp]: "G \<noteq> 0" "F \<noteq> 0"
-  have nz1: "fls_base_factor_to_fps F \<noteq> 0"
-    using \<open>F \<noteq> 0\<close> fls_base_factor_to_fps_nonzero by blast
-  show ?thesis
-    unfolding fls_compose_fps_def using nz1
-    by (subst fls_subdegree_mult) (simp_all add: fps_compose_eq_0_iff fls_subdegree_fls_to_fps)
-qed (auto simp: fls_compose_fps_0_right)
-
 lemma zorder_compose_aux:
   assumes "isolated_singularity_at f 0" "not_essential f 0"
   assumes G: "g has_fps_expansion G" "G \<noteq> 0" "g 0 = 0"
diff -r 3704717ed7bf -r ff4b062aae57 src/HOL/Computational_Algebra/Formal_Laurent_Series.thy
--- a/src/HOL/Computational_Algebra/Formal_Laurent_Series.thy	Mon Apr 21 08:24:58 2025 +0200
+++ b/src/HOL/Computational_Algebra/Formal_Laurent_Series.thy	Fri Apr 18 10:58:16 2025 +0200
@@ -1165,6 +1165,58 @@
   shows "fls_const x * fls_const y = fls_const (x*y)"
   by    (intro fls_eqI) simp
 
+lemma fls_subdegree_add_eq1:
+  assumes "f \<noteq> 0" "fls_subdegree f < fls_subdegree g"
+  shows   "fls_subdegree (f + g) = fls_subdegree f"
+proof (intro antisym)
+  from assms have *: "fls_nth (f + g) (fls_subdegree f) \<noteq> 0"
+    by auto
+  from * show "fls_subdegree (f + g) \<le> fls_subdegree f"
+    by (rule fls_subdegree_leI)
+  from * have "f + g \<noteq> 0"
+    using fls_nonzeroI by blast
+  thus "fls_subdegree f \<le> fls_subdegree (f + g)"
+    using assms(2) fls_plus_subdegree by force
+qed
+
+lemma fls_subdegree_add_eq2:
+  assumes "g \<noteq> 0" "fls_subdegree g < fls_subdegree f"
+  shows   "fls_subdegree (f + g) = fls_subdegree g"
+proof (intro antisym)
+  from assms have *: "fls_nth (f + g) (fls_subdegree g) \<noteq> 0"
+    by auto
+  from * show "fls_subdegree (f + g) \<le> fls_subdegree g"
+    by (rule fls_subdegree_leI)
+  from * have "f + g \<noteq> 0"
+    using fls_nonzeroI by blast
+  thus "fls_subdegree g \<le> fls_subdegree (f + g)"
+    using assms(2) fls_plus_subdegree by force
+qed
+
+lemma fls_subdegree_diff_eq1:
+  assumes "f \<noteq> 0" "fls_subdegree f < fls_subdegree g"
+  shows   "fls_subdegree (f - g) = fls_subdegree f"
+  using fls_subdegree_add_eq1[of f "-g"] assms by simp
+
+lemma fls_subdegree_diff_eq2:
+  assumes "g \<noteq> 0" "fls_subdegree g < fls_subdegree f"
+  shows   "fls_subdegree (f - g) = fls_subdegree g"
+  using fls_subdegree_add_eq2[of "-g" f] assms by simp
+
+lemma nat_minus_fls_subdegree_plus_const_eq:
+  "nat (-fls_subdegree (F + fls_const c)) = nat (-fls_subdegree F)"
+proof (cases "fls_subdegree F < 0")
+  case True
+  hence "fls_subdegree (F + fls_const c) = fls_subdegree F"
+    by (intro fls_subdegree_add_eq1) auto
+  thus ?thesis
+    by simp
+next
+  case False
+  thus ?thesis
+    by (auto simp: fls_subdegree_ge0I)
+qed
+
 lemma fls_mult_subdegree_ge:
   fixes   f g :: "'a::{comm_monoid_add,mult_zero} fls"
   assumes "f*g \<noteq> 0"
@@ -1705,6 +1757,13 @@
   by standard
 
 
+lemma fls_subdegree_numeral [simp]: "fls_subdegree (numeral n) = 0"
+  by (metis fls_subdegree_of_nat of_nat_numeral)
+
+lemma fls_regpart_numeral [simp]: "fls_regpart (numeral n) = numeral n"
+  by (metis fls_regpart_of_nat of_nat_numeral)
+
+
 subsubsection \<open>Powers\<close>
 
 lemma fls_subdegree_prod:
@@ -2946,6 +3005,20 @@
 instance fls :: ("{field_prime_char,comm_semiring_1}") field_prime_char
   by (rule field_prime_charI') auto
 
+instance fls :: (semiring_char_0) semiring_char_0
+proof
+  show "inj (of_nat :: nat \<Rightarrow> 'a fls)"
+    by (metis fls_regpart_of_nat injI of_nat_eq_iff)
+qed
+
+instance fls :: (field_char_0) field_char_0 ..
+
+
+lemma fls_subdegree_power_int [simp]:
+  fixes   F :: "'a :: field fls"
+  shows "fls_subdegree (F powi n) = n * fls_subdegree F"
+  by (auto simp: power_int_def fls_subdegree_pow)
+
 
 subsubsection \<open>Division\<close>
 
@@ -3440,45 +3513,6 @@
   shows   "fls_compose_fps (F - G) H = fls_compose_fps F H - fls_compose_fps G H"
   using fls_compose_fps_add[of H F "-G"] by simp
 
-lemma fps_compose_eq_0_iff:
-  fixes F G :: "'a :: idom fps"
-  assumes "fps_nth G 0 = 0"
-  shows "fps_compose F G = 0 \<longleftrightarrow> F = 0 \<or> (G = 0 \<and> fps_nth F 0 = 0)"
-proof safe
-  assume *: "fps_compose F G = 0" "F \<noteq> 0"
-  have "fps_nth (fps_compose F G) 0 = fps_nth F 0"
-    by simp
-  also have "fps_compose F G = 0"
-    by (simp add: *)
-  finally show "fps_nth F 0 = 0"
-    by simp
-  show "G = 0"
-  proof (rule ccontr)
-    assume "G \<noteq> 0"
-    hence "subdegree G > 0" using assms
-      using subdegree_eq_0_iff by blast
-    define N where "N = subdegree F * subdegree G"
-    have "fps_nth (fps_compose F G) N = (\<Sum>i = 0..N. fps_nth F i * fps_nth (G ^ i) N)"
-      unfolding fps_compose_def by (simp add: N_def)
-    also have "\<dots> = (\<Sum>i\<in>{subdegree F}. fps_nth F i * fps_nth (G ^ i) N)"
-    proof (intro sum.mono_neutral_right ballI)
-      fix i assume i: "i \<in> {0..N} - {subdegree F}"
-      show "fps_nth F i * fps_nth (G ^ i) N = 0"
-      proof (cases i "subdegree F" rule: linorder_cases)
-        assume "i > subdegree F"
-        hence "fps_nth (G ^ i) N = 0"
-          using i \<open>subdegree G > 0\<close> by (intro fps_pow_nth_below_subdegree) (auto simp: N_def)
-        thus ?thesis by simp
-      qed (use i in \<open>auto simp: N_def\<close>)
-    qed (use \<open>subdegree G > 0\<close> in \<open>auto simp: N_def\<close>)
-    also have "\<dots> = fps_nth F (subdegree F) * fps_nth (G ^ subdegree F) N"
-      by simp
-    also have "\<dots> \<noteq> 0"
-      using \<open>G \<noteq> 0\<close> \<open>F \<noteq> 0\<close> by (auto simp: N_def)
-    finally show False using * by auto
-  qed
-qed auto
-
 lemma fls_compose_fps_eq_0_iff:
   assumes "H \<noteq> 0" "fps_nth H 0 = 0"
   shows   "fls_compose_fps F H = 0 \<longleftrightarrow> F = 0"
@@ -3588,7 +3622,7 @@
   assumes "d > 0"
   shows   "fls_compose_power f d $$ n = (if int d dvd n then f $$ (n div int d) else 0)"
   by (simp add: assms fls_compose_power.rep_eq)
-     
+
 
 lemma fls_compose_power_0_left [simp]: "fls_compose_power 0 d = 0"
   by transfer auto
@@ -3680,6 +3714,20 @@
   "d dvd n \<Longrightarrow> d > 0 \<Longrightarrow> fls_compose_power f d $$ int n = f $$ int (n div d)"
   by (transfer; force; fail)+
 
+lemma subdegree_fls_compose_fps [simp]:
+  fixes G :: "'a :: field fps"
+  assumes [simp]: "fps_nth G 0 = 0"
+  shows "fls_subdegree (fls_compose_fps F G) = fls_subdegree F * subdegree G"
+proof (cases "F = 0"; cases "G = 0")
+  assume [simp]: "G \<noteq> 0" "F \<noteq> 0"
+  have nz1: "fls_base_factor_to_fps F \<noteq> 0"
+    using \<open>F \<noteq> 0\<close> fls_base_factor_to_fps_nonzero by blast
+  show ?thesis
+    unfolding fls_compose_fps_def using nz1
+    by (subst fls_subdegree_mult) (simp_all add: fps_compose_eq_0_iff fls_subdegree_fls_to_fps)
+qed (auto simp: fls_compose_fps_0_right)
+
+
 subsection \<open>Formal differentiation and integration\<close>
 
 subsubsection \<open>Derivative\<close>
@@ -3747,6 +3795,9 @@
   shows   "fls_subdegree (fls_deriv f) = fls_subdegree f - 1"
   by      (auto intro: fls_subdegree_deriv' simp: assms)
 
+lemma fps_deriv_fls_regpart: "fps_deriv (fls_regpart F) = fls_regpart (fls_deriv F)"
+  by (intro fps_ext) (auto simp: add_ac)
+
 text \<open>
   Shifting is like multiplying by a power of the implied variable, and so satisfies a product-like
   rule.
diff -r 3704717ed7bf -r ff4b062aae57 src/HOL/Computational_Algebra/Formal_Power_Series.thy
--- a/src/HOL/Computational_Algebra/Formal_Power_Series.thy	Mon Apr 21 08:24:58 2025 +0200
+++ b/src/HOL/Computational_Algebra/Formal_Power_Series.thy	Fri Apr 18 10:58:16 2025 +0200
@@ -11,6 +11,7 @@
   Complex_Main
   Euclidean_Algorithm
   Primes
+  "HOL-Library.FuncSet"
 begin
 
 
@@ -748,6 +749,19 @@
   from arg_cong[of _ _ "\<lambda>F. F $ 0", OF this] show False by simp
 qed 
 
+instance fps :: (semiring_char_0) semiring_char_0
+proof
+  show "inj (of_nat :: nat \<Rightarrow> 'a fps)"
+  proof
+    fix m n :: nat
+    assume "of_nat m = (of_nat n :: 'a fps)"
+    hence "fps_nth (of_nat m) 0 = (fps_nth (of_nat n) 0 :: 'a)"
+      by (simp only: )
+    thus "m = n"
+      by simp
+  qed
+qed
+
 lemma subdegree_power_ge:
   "f^n \<noteq> 0 \<Longrightarrow> subdegree (f^n) \<ge> n * subdegree f"
 proof (induct n)
@@ -801,6 +815,12 @@
   "subdegree ((f :: ('a :: semiring_1_no_zero_divisors) fps) ^ n) = n * subdegree f"
   by (cases "f = 0"; induction n) simp_all
 
+lemma subdegree_prod:
+  fixes f :: "'a \<Rightarrow> 'b :: idom fps"
+  assumes "\<And>x. x \<in> A \<Longrightarrow> f x \<noteq> 0"
+  shows   "subdegree (\<Prod>x\<in>A. f x) = (\<Sum>x\<in>A. subdegree (f x))"
+  using assms by (induction A rule: infinite_finite_induct) auto
+
 
 lemma minus_one_power_iff: "(- (1::'a::ring_1)) ^ n = (if even n then 1 else - 1)"
   by (induct n) auto
@@ -976,6 +996,25 @@
 qed simp_all
 
 
+subsection \<open>Truncation\<close>
+
+text \<open>
+  Truncation of formal power series: all monomials $cx^k$ with $k\geq n$ are removed;
+  the remainder is a polynomial of degree at most $n-1$.
+\<close>
+definition truncate_fps :: "nat \<Rightarrow> 'a fps \<Rightarrow> 'a :: zero fps" where
+  "truncate_fps n F = Abs_fps (\<lambda>k. if k \<ge> n then 0 else fps_nth F k)"
+
+lemma fps_nth_truncate' [simp]:
+  "k \<ge> n \<Longrightarrow> fps_nth (truncate_fps n F) k = 0"
+  "k < n \<Longrightarrow> fps_nth (truncate_fps n F) k = fps_nth F k"
+  by (auto simp: truncate_fps_def)
+
+lemma truncate_fps_eq_truncate_fps_iff:
+  "truncate_fps N F = truncate_fps N G \<longleftrightarrow> (\<forall>n<N. fps_nth F n = fps_nth G n)"
+  by (auto simp: fps_eq_iff truncate_fps_def)
+
+
 subsection \<open>Shifting and slicing\<close>
 
 definition fps_shift :: "nat \<Rightarrow> 'a fps \<Rightarrow> 'a fps" where
@@ -1402,6 +1441,144 @@
 lemma open_fps_def: "open (S :: 'a::group_add fps set) = (\<forall>a \<in> S. \<exists>r. r >0 \<and> {y. dist y a < r} \<subseteq> S)"
   unfolding open_dist subset_eq by simp
 
+
+text \<open>Topology\<close>
+
+subsection \<open>The topology of formal power series\<close>
+
+text \<open>
+  A set of formal power series is open iff for any power series $f$ in it, there exists some
+  number $n$ such that all power series that agree with $f$ on the first $n$ components are
+  also in it.
+\<close>
+lemma open_fps_iff:
+  "open A \<longleftrightarrow> (\<forall>F\<in>A. \<exists>n. {G. truncate_fps n G = truncate_fps n F} \<subseteq> A)"
+proof
+  assume "open A"
+  show "\<forall>F\<in>A. \<exists>n. {G. truncate_fps n G = truncate_fps n F} \<subseteq> A"
+  proof
+    fix F :: "'a fps"
+    assume F: "F \<in> A"
+    with \<open>open A\<close> obtain e where e: "e > 0" "\<And>G. dist G F < e \<Longrightarrow> G \<in> A"
+      by (force simp: open_fps_def)
+    thm dist_fps_def
+    have "filterlim (\<lambda>n. (1/2)^n :: real) (nhds 0) at_top"
+      by (intro LIMSEQ_realpow_zero) auto
+    from order_tendstoD(2)[OF this e(1)] have "eventually (\<lambda>n. 1 / 2 ^ n < e) at_top"
+      by (simp add: power_divide)
+    then obtain n where n: "1 / 2 ^ n < e"
+      by (auto simp: eventually_sequentially)
+    show "\<exists>n. {G. truncate_fps n G = truncate_fps n F} \<subseteq> A"
+    proof (rule exI[of _ n], safe)
+      fix G assume *: "truncate_fps n G = truncate_fps n F"
+      show "G \<in> A"
+      proof (cases "G = F")
+        case False
+        hence "dist G F = inverse (2 ^ subdegree (G - F))"
+          by (auto simp: dist_fps_def)
+        also have "subdegree (G - F) \<ge> n"
+        proof (rule subdegree_geI)
+          fix i assume "i < n"
+          hence "fps_nth (G - F) i = fps_nth (truncate_fps n G - truncate_fps n F) i"
+            by (auto simp: fps_eq_iff)
+          also from * have "\<dots> = 0"
+            by simp
+          finally show "fps_nth (G - F) i = 0" .
+        qed (use False in auto)
+        hence "inverse (2 ^ subdegree (G - F) :: real) \<le> inverse (2 ^ n)"
+          by (intro le_imp_inverse_le power_increasing) auto
+        also have "\<dots> < e"
+          using n by (simp add: field_simps)
+        finally show "G \<in> A"
+          using e(2)[of G] by auto
+      qed (use \<open>F \<in> A\<close> in auto)
+    qed
+  qed
+next
+  assume *: "\<forall>F\<in>A. \<exists>n. {G. truncate_fps n G = truncate_fps n F} \<subseteq> A"
+  show "open A"
+    unfolding open_fps_def
+  proof safe
+    fix F assume F: "F \<in> A"
+    with * obtain n where n: "\<And>G. truncate_fps n G = truncate_fps n F \<Longrightarrow> G \<in> A"
+      by blast
+    show "\<exists>r>0. {G. dist G F < r} \<subseteq> A"
+    proof (rule exI[of _ "1 / 2 ^ n"], safe)
+      fix G assume dist: "dist G F < 1 / 2 ^ n"
+      show "G \<in> A"
+      proof (cases "G = F")
+        case False
+        hence "dist G F = inverse (2 ^ subdegree (F - G))"
+          by (simp add: dist_fps_def)
+        with dist have "n < subdegree (F - G)"
+          by (auto simp: field_simps)
+        hence "fps_nth (F - G) i = 0" if "i \<le> n" for i
+          using that nth_less_subdegree_zero[of i "F - G"] by simp
+        hence "truncate_fps n G = truncate_fps n F"
+          by (auto simp: fps_eq_iff truncate_fps_def)
+        thus "G \<in> A"
+          by (rule n)
+      qed (use \<open>F \<in> A\<close> in auto)
+    qed auto
+  qed
+qed
+
+lemma open_truncate_fps: "open {H. truncate_fps N H = truncate_fps N G}"
+  unfolding open_fps_iff
+proof safe
+  fix F assume F: "truncate_fps N F = truncate_fps N G"
+  show "\<exists>n. {G. truncate_fps n G = truncate_fps n F}
+             \<subseteq> {H. truncate_fps N H = truncate_fps N G}"
+    by (rule exI[of _ N]) (use F in \<open>auto simp: fps_eq_iff\<close>)
+qed
+
+text \<open>
+  A family of formal power series $f_x$ tends to a limit series $g$ at some filter $F$
+  iff for any $N\geq 0$, the set of $x$ for which $f_x$ and $G$ agree on the first $N$ coefficients
+  is in $F$.
+
+  For a sequence $(f_i)_{n\geq 0}$ this means that $f_i \longrightarrow G$ iff for any 
+  $N\geq 0$, $f_x$ and $G$ agree for all but finitely many $x$.
+\<close>
+
+lemma tendsto_fps_iff:
+  "filterlim f (nhds (g :: 'a :: group_add fps)) F \<longleftrightarrow>
+     (\<forall>n. eventually (\<lambda>x. fps_nth (f x) n = fps_nth g n) F)"
+proof safe
+  assume lim: "filterlim f (nhds (g :: 'a :: group_add fps)) F"
+  show "eventually (\<lambda>x. fps_nth (f x) n = fps_nth g n) F" for n
+  proof -
+    define S where "S = {H. truncate_fps (n+1) H = truncate_fps (n+1) g}"
+    have S: "open S" "g \<in> S"
+      unfolding S_def using open_truncate_fps[of "n+1" g] by (auto simp: S_def)
+    from lim and S have "eventually (\<lambda>x. f x \<in> S) F"
+      using topological_tendstoD by blast
+    thus "eventually (\<lambda>x. fps_nth (f x) n = fps_nth g n) F"
+      by eventually_elim (auto simp: S_def truncate_fps_eq_truncate_fps_iff)
+  qed
+next
+  assume *: "\<forall>n. eventually (\<lambda>x. fps_nth (f x) n = fps_nth g n) F"
+  show "filterlim f (nhds (g :: 'a :: group_add fps)) F"
+  proof (rule topological_tendstoI)
+    fix S :: "'a fps set"
+    assume S: "open S" "g \<in> S"
+    then obtain N where N: "{H. truncate_fps N H = truncate_fps N g} \<subseteq> S"
+      unfolding open_fps_iff by blast
+    have "eventually (\<lambda>x. \<forall>n\<in>{..<N}. fps_nth (f x) n = fps_nth g n) F"
+      by (subst eventually_ball_finite_distrib) (use * in auto)
+    hence "eventually (\<lambda>x. f x \<in> {H. truncate_fps N H = truncate_fps N g}) F"
+      by eventually_elim (auto simp: truncate_fps_eq_truncate_fps_iff)
+    thus "eventually (\<lambda>x. f x \<in> S) F"
+      by eventually_elim (use N in auto)
+  qed
+qed
+
+lemma tendsto_fpsI:
+  assumes "\<And>n. eventually (\<lambda>x. fps_nth (f x) n = fps_nth G n) F"
+  shows   "filterlim f (nhds (G :: 'a :: group_add fps)) F"
+  unfolding tendsto_fps_iff using assms by blast
+
+
 text \<open>The infinite sums and justification of the notation in textbooks.\<close>
 
 lemma reals_power_lt_ex:
@@ -3447,6 +3624,333 @@
   by (simp add: fps_deriv_power' fps_of_nat)
 
 
+subsection \<open>Finite and infinite products\<close>
+
+text \<open>
+  The following operator gives the set of all functions $A \to \mathbb{N}$ with
+  $\sum_{x\in A} f(x) = n$, i.e.\ all the different ways to put $n$ unlabelled balls into
+  the labelled bins $A$.
+\<close>
+definition nat_partitions :: "'a set \<Rightarrow> nat \<Rightarrow> ('a \<Rightarrow> nat) set" where
+  "nat_partitions A n =
+     {f. finite {x. f x > 0} \<and> {x. f x > 0} \<subseteq> A \<and> (\<Sum>x\<in>{x\<in>A. f x > 0}. f x) = n}"
+
+lemma 
+  assumes "h \<in> nat_partitions A n"
+  shows   nat_partitions_outside: "x \<notin> A \<Longrightarrow> h x = 0"
+    and   nat_partitions_sum: "(\<Sum>x\<in>{x\<in>A. h x > 0}. h x) = n"
+    and   nat_partitions_finite_support: "finite {x. h x > 0}"
+  using assms by (auto simp: nat_partitions_def)
+
+lemma nat_partitions_finite_def:
+  assumes "finite A"
+  shows   "nat_partitions A n = {f. {x. f x > 0} \<subseteq> A \<and> (\<Sum>x\<in>A. f x) = n}"
+proof (intro equalityI subsetI)
+  fix f assume f: "f \<in> nat_partitions A n"
+  have "(\<Sum>x\<in>A. f x) = (\<Sum>x | x \<in> A \<and> f x > 0. f x)"
+    by (rule sum.mono_neutral_right) (use assms in auto)
+  thus "f \<in> {f. {x. f x > 0} \<subseteq> A \<and> (\<Sum>x\<in>A. f x) = n}"
+    using f nat_partitions_def by auto
+next
+  fix f assume "f \<in> {f. {x. f x > 0} \<subseteq> A \<and> (\<Sum>x\<in>A. f x) = n}"
+  hence f: "{x. f x > 0} \<subseteq> A" "(\<Sum>x\<in>A. f x) = n"
+    by blast+
+  have "(\<Sum>x\<in>A. f x) = (\<Sum>x | x \<in> A \<and> f x > 0. f x)"
+    by (rule sum.mono_neutral_right) (use assms in auto)
+  moreover have "finite {x. f x > 0}"
+    using f(1) assms by (rule finite_subset)
+  ultimately show "f \<in> nat_partitions A n"
+    using f by (simp add: nat_partitions_def)
+qed
+
+lemma nat_partitions_subset:
+  "nat_partitions A n \<subseteq> A \<rightarrow> {0..n}"
+proof
+  fix f assume f: "f \<in> nat_partitions A n"
+  have "f x \<le> n" if x: "x \<in> A" for x
+  proof (cases "f x = 0")
+    case False
+    have "f x \<le> (\<Sum>x\<in>{x\<in>A. f x \<noteq> 0}. f x)"
+      by (rule member_le_sum) (use x False f in \<open>auto simp: nat_partitions_def\<close>)
+    also have "\<dots> = n"
+      using f by (auto simp: nat_partitions_def)
+    finally show "f x \<le> n" .
+  qed auto
+  thus "f \<in> A \<rightarrow> {0..n}"
+    using f by (auto simp: nat_partitions_def)
+qed
+
+lemma conj_mono_strong: "(P1 \<longrightarrow> Q1) \<Longrightarrow> (P1 \<longrightarrow> P2 \<longrightarrow> Q2) \<Longrightarrow> (P1 \<and> P2) \<longrightarrow> (Q1 \<and> Q2)"
+  by iprover
+
+lemma nat_partitions_mono:
+  assumes "A \<subseteq> B"
+  shows   "nat_partitions A n \<subseteq> nat_partitions B n"
+  unfolding nat_partitions_def
+proof (intro Collect_mono conj_mono_strong impI)
+  fix f :: "'a \<Rightarrow> nat"
+  assume 1: "finite {x. f x > 0}"
+  assume 2: "{x. f x > 0} \<subseteq> A"
+  thus "{x. f x > 0} \<subseteq> B"
+    using assms by blast
+  assume 3: "(\<Sum>x | x \<in> A \<and> f x > 0. f x) = n"
+  have *: "{x\<in>B. f x > 0} = {x\<in>A. f x > 0} \<union> {x\<in>B-A. f x > 0}"
+    using assms by auto
+  have "(\<Sum>x | x \<in> B \<and> f x > 0. f x) = (\<Sum>x | x \<in> A \<and> f x > 0. f x)"
+    by (intro sum.mono_neutral_right) (use assms 2 in \<open>auto intro: finite_subset[OF _ 1]\<close>)
+  with 3 show "(\<Sum>x | x \<in> B \<and> f x > 0. f x) = n"
+    by simp
+qed
+
+lemma in_nat_partitions_imp_le:
+  assumes "h \<in> nat_partitions A n" "x \<in> A"
+  shows   "h x \<le> n"
+  using nat_partitions_subset[of A n] assms by (auto simp: PiE_def Pi_def)
+
+lemma nat_partitions_0 [simp]: "nat_partitions A 0 = {\<lambda>_. 0}"
+proof (intro equalityI subsetI)
+  fix h :: "'a \<Rightarrow> nat" assume "h \<in> {\<lambda>_. 0}"
+  thus "h \<in> nat_partitions A 0"
+    by (auto simp: nat_partitions_def)
+qed (auto simp: nat_partitions_def fun_eq_iff)
+
+lemma nat_partitions_empty [simp]: "n > 0 \<Longrightarrow> nat_partitions {} n = {}"
+  by (auto simp: nat_partitions_def fun_eq_iff)
+
+lemma nat_partitions_insert:
+  assumes [simp]: "a \<notin> A"
+  shows   "bij_betw (\<lambda>(m,f). f(a := m))
+             (SIGMA m:{0..n}. nat_partitions A (n - m)) (nat_partitions (insert a A) n)"
+proof (rule bij_betwI[of _ _ _ "\<lambda>f. (f a, f(a := 0))"], goal_cases)
+  case 1
+  show ?case
+  proof safe
+    fix m f assume m: "m \<in> {0..n}" and f: "f \<in> nat_partitions A (n - m)"
+    define f' where "f' = f(a := m)"
+    have "(\<Sum>x\<in>{x\<in>insert a A. f' x > 0}. f' x) = (\<Sum>x\<in>insert a {x\<in>A. f x > 0}. f' x)"
+      by (rule sum.mono_neutral_cong_left)
+         (use f in \<open>auto simp: f'_def nat_partitions_def\<close>)
+    also have "\<dots> = m + (\<Sum>x\<in>{x\<in>A. f x > 0}. f' x)"
+      by (subst sum.insert) (use f in \<open>auto simp: nat_partitions_def f'_def\<close>)
+    also have "(\<Sum>x\<in>{x\<in>A. f x > 0}. f' x) = (\<Sum>x\<in>{x\<in>A. f x > 0}. f x)"
+      by (intro sum.cong) (auto simp: f'_def)
+    also have "\<dots> = n - m"
+      using f by (auto simp: nat_partitions_def)
+    finally have "(\<Sum>x\<in>{x\<in>insert a A. f' x > 0}. f' x) = n"
+      using m by simp
+    moreover have "finite {x. f' x > 0}"
+      by (rule finite_subset[of _ "insert a {x\<in>A. f x > 0}"])
+         (use f in \<open>auto simp: nat_partitions_def f'_def\<close>)
+    moreover have "{x. f' x > 0} \<subseteq> insert a A"
+      using f by (auto simp: f'_def nat_partitions_def)
+    ultimately show "f' \<in> nat_partitions (insert a A) n"
+      by (simp add: nat_partitions_def)
+  qed
+next
+  case 2
+  show ?case
+  proof safe
+    fix f assume "f \<in> nat_partitions (insert a A) n"
+    define f' where "f' = f(a := 0)"
+    have  fin: "finite {x. f x > 0}"
+      and subset: "{x. f x > 0} \<subseteq> insert a A"
+      and sum: "(\<Sum>x\<in>{x\<in>insert a A. f x > 0}. f x) = n"
+      using \<open>f \<in> _\<close> by (auto simp: nat_partitions_def)
+
+    show le: "f a \<in> {0..n}"
+    proof (cases "f a = 0")
+      case False
+      hence "f a \<le> (\<Sum>x\<in>{x\<in>insert a A. f x > 0}. f x)"
+        by (intro member_le_sum) (use fin in auto)
+      with sum show ?thesis
+        by simp
+    qed auto
+
+    have "n = (\<Sum>x\<in>{x\<in>insert a A. f x > 0}. f x)"
+      using sum by simp
+    also have "(\<Sum>x\<in>{x\<in>insert a A. f x > 0}. f x) = (\<Sum>x\<in>insert a {x\<in>A. f x > 0}. f x)"
+      by (rule sum.mono_neutral_left) (auto intro: finite_subset[OF _ fin])
+    also have "\<dots> = f a + (\<Sum>x\<in>{x\<in>A. f x > 0}. f x)"
+      by (subst sum.insert) (auto intro: finite_subset[OF _ fin])
+    also have "(\<Sum>x\<in>{x\<in>A. f x > 0}. f x) = (\<Sum>x\<in>{x\<in>A. f' x > 0}. f' x)"
+      by (intro sum.cong) (auto simp: f'_def)
+    finally have "(\<Sum>x\<in>{x\<in>A. f' x > 0}. f' x) = n - f a"
+      using le by simp
+
+    moreover have "finite {x. 0 < f' x}"
+      by (rule finite_subset[OF _ fin]) (auto simp: f'_def)
+    moreover have "{x. 0 < f' x} \<subseteq> A"
+      using subset by (auto simp: f'_def)
+    ultimately show "f' \<in> nat_partitions A (n - f a)"
+      by (auto simp: nat_partitions_def)
+  qed
+next
+  case (3 f)
+  thus ?case
+    by (fastforce simp: nat_partitions_def fun_eq_iff)
+qed (auto simp: nat_partitions_def)
+
+lemma finite_nat_partitions [intro]:
+  assumes "finite A"
+  shows   "finite (nat_partitions A n)"
+  using assms
+proof (induction arbitrary: n rule: finite_induct)
+  case empty
+  thus ?case
+    by (cases "n = 0") auto
+next
+  case (insert x A n)
+  have "finite (SIGMA m:{0..n}. nat_partitions A (n - m))"
+    by (auto intro: insert.IH)
+  also have "?this \<longleftrightarrow> finite (nat_partitions (insert x A) n)"
+    by (rule bij_betw_finite, rule nat_partitions_insert) fact
+  finally show ?case .
+qed
+
+lemma fps_prod_nth':
+  assumes "finite A"
+  shows   "fps_nth (\<Prod>x\<in>A. f x) n = (\<Sum>h\<in>nat_partitions A n. \<Prod>x\<in>A. fps_nth (f x) (h x))"
+  using assms
+proof (induction A arbitrary: n rule: finite_induct)
+  case (insert a A n)
+  note [simp] = \<open>a \<notin> A\<close>
+  note [intro, simp] = \<open>finite A\<close>
+  have "(\<Sum>h\<in>nat_partitions (insert a A) n. \<Prod>x\<in>insert a A. fps_nth (f x) (h x)) =
+        (\<Sum>(m,h)\<in>(SIGMA m:{0..n}. nat_partitions A (n-m)). \<Prod>x\<in>insert a A. fps_nth (f x) ((h(a := m)) x))"
+    by (subst sum.reindex_bij_betw[OF nat_partitions_insert, symmetric])
+       (simp_all add: case_prod_unfold)
+  also have "\<dots> = (\<Sum>m=0..n. \<Sum>h\<in>nat_partitions A (n-m). \<Prod>x\<in>insert a A. fps_nth (f x) ((h(a := m)) x))"
+    by (rule sum.Sigma [symmetric]) auto
+  also have "\<dots> = (\<Sum>m=0..n. fps_nth (f a) m * fps_nth (\<Prod>x\<in>A. f x) (n - m))"
+  proof (rule sum.cong)
+    fix m
+    assume m: "m \<in> {0..n}"
+    have "(\<Sum>h\<in>nat_partitions A (n-m). \<Prod>x\<in>insert a A. fps_nth (f x) ((h(a := m)) x)) =
+          fps_nth (f a) m * (\<Sum>h\<in>nat_partitions A (n-m). \<Prod>x\<in>A. fps_nth (f x) ((h(a := m)) x))"
+      by (simp add: sum_distrib_left)
+    also have "(\<Sum>h\<in>nat_partitions A (n-m). \<Prod>x\<in>A. fps_nth (f x) ((h(a := m)) x)) =
+               (\<Sum>h\<in>nat_partitions A (n-m). \<Prod>x\<in>A. fps_nth (f x) (h x))"
+      by (intro sum.cong prod.cong) auto
+    also have "\<dots> = fps_nth (\<Prod>x\<in>A. f x) (n - m)"
+      by (rule insert.IH [symmetric])
+    finally show "(\<Sum>h\<in>nat_partitions A (n-m). \<Prod>x\<in>insert a A. fps_nth (f x) ((h(a := m)) x)) = 
+                    fps_nth (f a) m * fps_nth (\<Prod>x\<in>A. f x) (n - m)" .
+  qed auto
+  also have "\<dots> = fps_nth (\<Prod>x\<in>insert a A. f x) n"
+    by (simp add: fps_mult_nth)
+  finally show ?case ..
+qed auto
+
+theorem tendsto_prod_fps:
+  fixes f :: "nat \<Rightarrow> 'a :: {idom,  t2_space} fps"
+  assumes [simp]: "\<And>k. f k \<noteq> 0"
+  assumes g: "\<And>n k. k > g n \<Longrightarrow> subdegree (f k - 1) > n"
+  defines "P \<equiv> Abs_fps (\<lambda>n. (\<Sum>h\<in>nat_partitions {..g n} n. \<Prod>i\<le>g n. fps_nth (f i) (h i)))"
+  shows   "(\<lambda>n. \<Prod>k\<le>n. f k) \<longlonglongrightarrow> P"
+proof (rule tendsto_fpsI)
+  fix n :: nat
+  show "eventually (\<lambda>N. fps_nth (prod f {..N}) n = fps_nth P n) at_top"
+    using eventually_ge_at_top[of "g n"]
+  proof eventually_elim
+    case (elim N)
+    have "fps_nth (prod f {..N}) n = (\<Sum>h\<in>nat_partitions {..N} n. \<Prod>x\<le>N. fps_nth (f x) (h x))"
+      by (subst fps_prod_nth') auto
+    also have "\<dots> = (\<Sum>h | h \<in> nat_partitions {..N} n \<and> (\<forall>x\<le>N. fps_nth (f x) (h x) \<noteq> 0). 
+                      \<Prod>x\<le>N. fps_nth (f x) (h x))"
+      by (intro sum.mono_neutral_right) auto
+
+    also have "{h. h \<in> nat_partitions {..N} n \<and> (\<forall>x\<le>N. fps_nth (f x) (h x) \<noteq> 0)} =
+               {h. h \<in> nat_partitions {..g n} n \<and> (\<forall>x\<le>N. fps_nth (f x) (h x) \<noteq> 0)}" (is "?lhs = ?rhs")
+    proof (intro equalityI subsetI)
+      fix h assume "h \<in> ?rhs"
+      thus "h \<in> ?lhs" using elim nat_partitions_mono[of "{..g n}" "{..N}"] by auto
+    next
+      fix h assume "h \<in> ?lhs"
+      hence h: "{x. 0 < h x} \<subseteq> {..N}" "(\<Sum>x\<le>N. h x) = n" "\<And>x. x \<le> N \<Longrightarrow> fps_nth (f x) (h x) \<noteq> 0"
+        by (auto simp: nat_partitions_finite_def)
+      have "{x. 0 < h x} \<subseteq> {..g n}"
+      proof
+        fix x assume *: "x \<in> {x. h x > 0}"
+        show "x \<in> {..g n}"
+        proof (rule ccontr)
+          assume "x \<notin> {..g n}"
+          hence x: "x > g n" "x \<le> N"
+            using h(1) * by auto
+          have "h x \<le> n"
+            using \<open>h \<in> ?lhs\<close> nat_partitions_subset[of "{..N}" n] x by (auto simp: Pi_def)
+          also have "n < subdegree (f x - 1)"
+            by (rule g) (use x in auto)
+          finally have "fps_nth (f x - 1) (h x) = 0"
+            by blast
+          hence "fps_nth (f x) (h x) = 0"
+            using * by simp
+          moreover have "fps_nth (f x) (h x) \<noteq> 0"
+            by (intro h(3)) (use x in auto)
+          ultimately show False by contradiction
+        qed
+      qed
+      moreover from this have "(\<Sum>x\<le>N. h x) = (\<Sum>x\<le>g n. h x)"
+        by (intro sum.mono_neutral_right) (use elim in auto)
+      ultimately show "h \<in> ?rhs" using elim h
+        by (auto simp: nat_partitions_finite_def)
+    qed
+
+    also have "(\<Sum>h | h \<in> nat_partitions {..g n} n \<and> (\<forall>x\<le>N. fps_nth (f x) (h x) \<noteq> 0). 
+                      \<Prod>x\<le>N. fps_nth (f x) (h x)) = 
+               (\<Sum>h | h \<in> nat_partitions {..g n} n \<and> (\<forall>x\<le>N. fps_nth (f x) (h x) \<noteq> 0). 
+                      \<Prod>i\<le>g n. fps_nth (f i) (h i))"
+    proof (intro sum.cong prod.mono_neutral_right ballI)
+      fix h i 
+      assume i: "i \<in> {..N} - {..g n}"
+      assume "h \<in> {h. h \<in> nat_partitions {..g n} n \<and> (\<forall>x\<le>N. fps_nth (f x) (h x) \<noteq> 0)}"
+      hence h: "h \<in> nat_partitions {..g n} n" "\<And>x. x \<le> N \<Longrightarrow> fps_nth (f x) (h x) \<noteq> 0"
+        by blast+
+      have [simp]: "h i = 0"
+        using i h unfolding nat_partitions_def by auto
+      have "n < subdegree (f i - 1)"
+        by (intro g) (use i in auto)
+      moreover have "h i \<le> n"
+        by auto
+      ultimately have "fps_nth (f i - 1) (h i) = 0"
+        by (intro nth_less_subdegree_zero) auto
+      thus "fps_nth (f i) (h i) = 1"
+        using h(2) i by (auto split: if_splits)
+    qed (use elim in auto)
+
+    also have "(\<Sum>h | h \<in> nat_partitions {..g n} n \<and> (\<forall>x\<le>N. fps_nth (f x) (h x) \<noteq> 0). 
+                   \<Prod>i\<le>g n. fps_nth (f i) (h i)) =
+               (\<Sum>h \<in> nat_partitions {..g n} n. \<Prod>i\<le>g n. fps_nth (f i) (h i))"
+    proof (intro sum.mono_neutral_left ballI)
+      fix h assume "h \<in> nat_partitions {..g n} n - {h\<in>nat_partitions {..g n} n. \<forall>x\<le>N. fps_nth (f x) (h x) \<noteq> 0}"
+      then obtain i where h: "h \<in> nat_partitions {..g n} n" and i: "i \<le> N" "fps_nth (f i) (h i) = 0"
+        by blast
+      have "\<not>(i > g n)"
+      proof
+        assume i': "i > g n"
+        hence "h i = 0"
+          using h by (auto simp: nat_partitions_def)
+        have "subdegree (f i - 1) > n"
+          by (intro g) (use i' in auto)
+        hence "subdegree (f i - 1) > 0"
+          by simp
+        hence "fps_nth (f i - 1) 0 = 0"
+          by blast
+        hence "fps_nth (f i) (h i) = 1"
+          using \<open>h i = 0\<close> by simp
+        thus False using i by simp
+      qed
+      thus " (\<Prod>x\<le>g n. fps_nth (f x) (h x)) = 0"
+        using i by auto
+    qed auto
+
+    also have "\<dots> = fps_nth P n"
+      by (simp add: P_def)
+    finally show "fps_nth (\<Prod>k\<le>N. f k) n = fps_nth P n" .
+  qed
+qed
+
+
+
 subsection \<open>Integration\<close>
 
 definition fps_integral :: "'a::{semiring_1,inverse} fps \<Rightarrow> 'a \<Rightarrow> 'a fps"
@@ -4911,6 +5415,64 @@
 lemma fps_X_fps_compose: "fps_X oo a = Abs_fps (\<lambda>n. if n = 0 then (0::'a::comm_ring_1) else a$n)"
   by (simp add: fps_eq_iff fps_compose_nth mult_delta_left)
 
+lemma fps_compose_eq_0_iff:
+  fixes F G :: "'a :: idom fps"
+  assumes "fps_nth G 0 = 0"
+  shows "fps_compose F G = 0 \<longleftrightarrow> F = 0 \<or> (G = 0 \<and> fps_nth F 0 = 0)"
+proof safe
+  assume *: "fps_compose F G = 0" "F \<noteq> 0"
+  have "fps_nth (fps_compose F G) 0 = fps_nth F 0"
+    by simp
+  also have "fps_compose F G = 0"
+    by (simp add: *)
+  finally show "fps_nth F 0 = 0"
+    by simp
+  show "G = 0"
+  proof (rule ccontr)
+    assume "G \<noteq> 0"
+    hence "subdegree G > 0" using assms
+      using subdegree_eq_0_iff by blast
+    define N where "N = subdegree F * subdegree G"
+    have "fps_nth (fps_compose F G) N = (\<Sum>i = 0..N. fps_nth F i * fps_nth (G ^ i) N)"
+      unfolding fps_compose_def by (simp add: N_def)
+    also have "\<dots> = (\<Sum>i\<in>{subdegree F}. fps_nth F i * fps_nth (G ^ i) N)"
+    proof (intro sum.mono_neutral_right ballI)
+      fix i assume i: "i \<in> {0..N} - {subdegree F}"
+      show "fps_nth F i * fps_nth (G ^ i) N = 0"
+      proof (cases i "subdegree F" rule: linorder_cases)
+        assume "i > subdegree F"
+        hence "fps_nth (G ^ i) N = 0"
+          using i \<open>subdegree G > 0\<close> by (intro fps_pow_nth_below_subdegree) (auto simp: N_def)
+        thus ?thesis by simp
+      qed (use i in \<open>auto simp: N_def\<close>)
+    qed (use \<open>subdegree G > 0\<close> in \<open>auto simp: N_def\<close>)
+    also have "\<dots> = fps_nth F (subdegree F) * fps_nth (G ^ subdegree F) N"
+      by simp
+    also have "\<dots> \<noteq> 0"
+      using \<open>G \<noteq> 0\<close> \<open>F \<noteq> 0\<close> by (auto simp: N_def)
+    finally show False using * by auto
+  qed
+qed auto
+
+lemma subdegree_fps_compose [simp]:
+  fixes F G :: "'a :: idom fps"
+  assumes [simp]: "fps_nth G 0 = 0"
+  shows "subdegree (fps_compose F G) = subdegree F * subdegree G"
+proof (cases "G = 0"; cases "F = 0")
+  assume [simp]: "G \<noteq> 0" "F \<noteq> 0"
+  define m where "m = subdegree F"
+  define F' where "F' = fps_shift m F"
+  have F_eq: "F = F' * fps_X ^ m"
+    unfolding F'_def by (simp add: fps_shift_times_fps_X_power m_def)
+  have [simp]: "F' \<noteq> 0"
+    using \<open>F \<noteq> 0\<close> unfolding F_eq by auto
+  have "subdegree (fps_compose F G) = subdegree (fps_compose F' G) + m * subdegree G"
+    by (simp add: F_eq fps_compose_mult_distrib fps_compose_eq_0_iff flip: fps_compose_power)
+  also have "subdegree (fps_compose F' G) = 0"
+    by (intro subdegree_eq_0) (auto simp: F'_def m_def)
+  finally show ?thesis by (simp add: m_def)
+qed auto
+
 lemma fps_inverse_compose:
   assumes b0: "(b$0 :: 'a::field) = 0"
     and a0: "a$0 \<noteq> 0"
diff -r 3704717ed7bf -r ff4b062aae57 src/HOL/Groups_Big.thy
--- a/src/HOL/Groups_Big.thy	Mon Apr 21 08:24:58 2025 +0200
+++ b/src/HOL/Groups_Big.thy	Fri Apr 18 10:58:16 2025 +0200
@@ -1792,4 +1792,74 @@
   finally show ?case .
 qed
 
+lemma prod_add:
+  fixes f1 f2 :: "'a \<Rightarrow> 'c :: comm_semiring_1"
+  assumes finite: "finite A"
+  shows   "(\<Prod>x\<in>A. f1 x + f2 x) = (\<Sum>X\<in>Pow A. (\<Prod>x\<in>X. f1 x) * (\<Prod>x\<in>A-X. f2 x))"
+  using assms
+proof (induction A rule: finite_induct)
+  case (insert x A)
+  have "(\<Sum>X\<in>Pow (insert x A). (\<Prod>x\<in>X. f1 x) * (\<Prod>x\<in>insert x A-X. f2 x)) =
+        (\<Sum>X\<in>Pow A. (\<Prod>x\<in>X. f1 x) * (\<Prod>x\<in>insert x A-X. f2 x)) +
+        (\<Sum>X\<in>insert x ` (Pow A). (\<Prod>x\<in>X. f1 x) * (\<Prod>x\<in>insert x A-X. f2 x))"
+    unfolding Pow_insert by (rule sum.union_disjoint) (use insert.hyps in auto)
+  also have "(\<Sum>X\<in>Pow A. (\<Prod>x\<in>X. f1 x) * (\<Prod>x\<in>insert x A-X. f2 x)) =
+             (\<Sum>X\<in>Pow A. f2 x * (\<Prod>x\<in>X. f1 x) * (\<Prod>x\<in>A-X. f2 x))"
+  proof (rule sum.cong)
+    fix X assume X: "X \<in> Pow A"
+    have "(\<Prod>x\<in>X. f1 x) * (\<Prod>x\<in>insert x (A-X). f2 x) = f2 x * (\<Prod>x\<in>X. f1 x) * (\<Prod>x\<in>A-X. f2 x)"
+      by (subst prod.insert) (use insert.hyps finite_subset[of X A] X in \<open>auto simp: mult_ac\<close>)
+    also have "insert x (A - X) = insert x A - X"
+      using insert.hyps X by auto
+    finally show "(\<Prod>x\<in>X. f1 x) * (\<Prod>x\<in>insert x A-X. f2 x) = f2 x * (\<Prod>x\<in>X. f1 x) * (\<Prod>x\<in>A-X. f2 x)" .
+  qed auto
+  also have "(\<Sum>X\<in>insert x ` (Pow A). (\<Prod>x\<in>X. f1 x) * (\<Prod>x\<in>insert x A-X. f2 x)) = 
+             (\<Sum>X\<in>Pow A. (\<Prod>x\<in>insert x X. f1 x) * (\<Prod>x\<in>insert x A-insert x X. f2 x))"
+    by (subst sum.reindex) (use insert.hyps in \<open>auto intro!: inj_onI simp: o_def\<close>)
+  also have "(\<Sum>X\<in>Pow A. (\<Prod>x\<in>insert x X. f1 x) * (\<Prod>x\<in>insert x A-insert x X. f2 x)) =
+             (\<Sum>X\<in>Pow A. f1 x * (\<Prod>x\<in>X. f1 x) * (\<Prod>x\<in>A-X. f2 x))"
+  proof (rule sum.cong)
+    fix X assume X: "X \<in> Pow A"
+    show "(\<Prod>x\<in>insert x X. f1 x) * (\<Prod>x\<in>insert x A-insert x X. f2 x) = 
+          f1 x * (\<Prod>x\<in>X. f1 x) * (\<Prod>x\<in>A-X. f2 x)"
+      by (subst prod.insert) (use insert.hyps finite_subset[of X A] X in auto)
+  qed auto
+  also have "(\<Sum>X\<in>Pow A. f2 x * prod f1 X * prod f2 (A - X)) + 
+             (\<Sum>X\<in>Pow A. f1 x * prod f1 X * prod f2 (A - X)) =
+             (f1 x + f2 x) * (\<Sum>X\<in>Pow A. prod f1 X * prod f2 (A - X))"
+    by (simp add: algebra_simps flip: sum_distrib_left sum_distrib_right)
+  finally show ?case
+    by (subst (asm) insert.IH [symmetric]) (use insert.hyps in simp)
+qed auto
+
+lemma prod_diff1:
+  fixes f1 f2 :: "'a \<Rightarrow> 'c :: comm_ring_1"
+  assumes finite: "finite A"
+  shows   "(\<Prod>x\<in>A. f1 x - f2 x) = (\<Sum>X\<in>Pow A. (-1) ^ card X * (\<Prod>x\<in>X. f2 x) * (\<Prod>x\<in>A-X. f1 x))"
+proof -
+  have "(\<Prod>x\<in>A. f1 x - f2 x) = (\<Prod>x\<in>A. -f2 x + f1 x)"
+    by simp
+  also have "\<dots> = (\<Sum>X\<in>Pow A. (\<Prod>x\<in>X. - f2 x) * prod f1 (A - X))"
+    by (rule prod_add) fact+
+  also have "\<dots> = (\<Sum>X\<in>Pow A. (-1) ^ card X * (\<Prod>x\<in>X. f2 x) * prod f1 (A - X))"
+    by (simp add: prod_uminus)
+  finally show ?thesis .
+qed
+
+lemma prod_diff2:
+  fixes f1 f2 :: "'a \<Rightarrow> 'c :: comm_ring_1"
+  assumes finite: "finite A"
+  shows   "(\<Prod>x\<in>A. f1 x - f2 x) = (\<Sum>X\<in>Pow A. (-1) ^ (card A - card X) * (\<Prod>x\<in>X. f1 x) * (\<Prod>x\<in>A-X. f2 x))"
+proof -
+  have "(\<Prod>x\<in>A. f1 x - f2 x) = (\<Prod>x\<in>A. f1 x + (-f2 x))"
+    by simp
+  also have "\<dots> = (\<Sum>X\<in>Pow A. (\<Prod>x\<in>X. f1 x) * (\<Prod>x\<in>A-X. -f2 x))"
+    by (rule prod_add) fact+
+  also have "\<dots> = (\<Sum>X\<in>Pow A. (-1) ^ card (A - X) * (\<Prod>x\<in>X. f1 x) * (\<Prod>x\<in>A-X. f2 x))"
+    by (simp add: prod_uminus mult_ac)
+  also have "\<dots> = (\<Sum>X\<in>Pow A. (-1) ^ (card A - card X) * (\<Prod>x\<in>X. f1 x) * (\<Prod>x\<in>A-X. f2 x))"
+    using finite_subset[OF _ assms] by (intro sum.cong refl, subst card_Diff_subset) auto
+  finally show ?thesis .
+qed
+
 end
diff -r 3704717ed7bf -r ff4b062aae57 src/HOL/Library/FuncSet.thy
--- a/src/HOL/Library/FuncSet.thy	Mon Apr 21 08:24:58 2025 +0200
+++ b/src/HOL/Library/FuncSet.thy	Fri Apr 18 10:58:16 2025 +0200
@@ -810,4 +810,37 @@
     by blast
 qed
 
+subsection \<open>Products of sums\<close>
+
+lemma prod_sum_PiE:
+  fixes f :: "'a \<Rightarrow> 'b \<Rightarrow> 'c :: comm_semiring_1"
+  assumes finite: "finite A" and finite: "\<And>x. x \<in> A \<Longrightarrow> finite (B x)"
+  shows   "(\<Prod>x\<in>A. \<Sum>y\<in>B x. f x y) = (\<Sum>g\<in>PiE A B. \<Prod>x\<in>A. f x (g x))"
+  using assms
+proof (induction A rule: finite_induct)
+  case empty
+  thus ?case by auto
+next
+  case (insert x A)
+  have "(\<Sum>g\<in>Pi\<^sub>E (insert x A) B. \<Prod>x\<in>insert x A. f x (g x)) =
+          (\<Sum>g\<in>Pi\<^sub>E (insert x A) B. f x (g x) * (\<Prod>x'\<in>A. f x' (g x')))"
+    using insert by simp
+  also have "(\<lambda>g. \<Prod>x'\<in>A. f x' (g x')) = (\<lambda>g. \<Prod>x'\<in>A. f x' (if x' = x then undefined else g x'))"
+    using insert by (intro ext prod.cong) auto
+  also have "(\<Sum>g\<in>Pi\<^sub>E (insert x A) B. f x (g x) * \<dots> g) =
+               (\<Sum>(y,g)\<in>B x \<times> Pi\<^sub>E A B. f x y * (\<Prod>x'\<in>A. f x' (g x')))"
+    using insert.prems insert.hyps
+    by (intro sum.reindex_bij_witness[of _ "\<lambda>(y,g). g(x := y)" "\<lambda>g. (g x, g(x := undefined))"])
+       (auto simp: PiE_def extensional_def)
+  also have "\<dots> = (\<Sum>y\<in>B x. \<Sum>g\<in>Pi\<^sub>E A B. f x y * (\<Prod>x'\<in>A. f x' (g x')))"
+    by (subst sum.cartesian_product) auto
+  also have "\<dots> = (\<Sum>y\<in>B x. f x y) * (\<Sum>g\<in>Pi\<^sub>E A B. \<Prod>x'\<in>A. f x' (g x'))"
+    using insert by (subst sum.swap) (simp add: sum_distrib_left sum_distrib_right)
+  also have "(\<Sum>g\<in>Pi\<^sub>E A B. \<Prod>x'\<in>A. f x' (g x')) = (\<Prod>x\<in>A. \<Sum>y\<in>B x. f x y)"
+    using insert.prems by (intro insert.IH [symmetric]) auto
+  also have "(\<Sum>y\<in>B x. f x y) * \<dots> = (\<Prod>x\<in>insert x A. \<Sum>y\<in>B x. f x y)"
+    using insert.hyps by simp
+  finally show ?case ..
+qed
+
 end