diff -r f82639fe786e -r 4c1347e172b1 src/HOL/Rat.thy
--- a/src/HOL/Rat.thy	Sat Mar 30 01:12:48 2024 +0100
+++ b/src/HOL/Rat.thy	Fri Mar 29 19:28:59 2024 +0100
@@ -877,6 +877,12 @@
   for a :: "'a::field_char_0"
   by (metis Rats_cases Rats_of_rat of_rat_power)
 
+lemma Rats_sum [intro]: "(\<And>x. x \<in> A \<Longrightarrow> f x \<in> \<rat>) \<Longrightarrow> sum f A \<in> \<rat>"
+  by (induction A rule: infinite_finite_induct) auto
+
+lemma Rats_prod [intro]: "(\<And>x. x \<in> A \<Longrightarrow> f x \<in> \<rat>) \<Longrightarrow> prod f A \<in> \<rat>"
+  by (induction A rule: infinite_finite_induct) auto
+
 lemma Rats_induct [case_names of_rat, induct set: Rats]: "q \<in> \<rat> \<Longrightarrow> (\<And>r. P (of_rat r)) \<Longrightarrow> P q"
   by (rule Rats_cases) auto