Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/HOL/Rat.thy
changeset 80061 4c1347e172b1
parent 77179 6d2ca97a8f46 
--- 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
isabelle