--- a/src/HOL/Complex.thy Sun Sep 24 15:55:42 2023 +0200
+++ b/src/HOL/Complex.thy Mon Sep 25 17:06:05 2023 +0100
@@ -769,6 +769,14 @@
lemma Im_sum[simp]: "Im (sum f s) = (\<Sum>x\<in>s. Im(f x))"
by (induct s rule: infinite_finite_induct) auto
+lemma Rats_complex_of_real_iff [iff]: "complex_of_real x \<in> \<rat> \<longleftrightarrow> x \<in> \<rat>"
+proof -
+ have "\<And>a b. \<lbrakk>0 < b; x = complex_of_int a / complex_of_int b\<rbrakk> \<Longrightarrow> x \<in> \<rat>"
+ by (metis Rats_divide Rats_of_int Re_complex_of_real Re_divide_of_real of_real_of_int_eq)
+ then show ?thesis
+ by (auto simp: elim!: Rats_cases')
+qed
+
lemma sum_Re_le_cmod: "(\<Sum>i\<in>I. Re (z i)) \<le> cmod (\<Sum>i\<in>I. z i)"
by (metis Re_sum complex_Re_le_cmod)