diff -r e10ef4f9c848 -r 1b9388e6eb75 src/HOL/Complex.thy
--- 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)