--- a/src/HOL/Complex.thy Tue Aug 31 13:54:31 2021 +0200
+++ b/src/HOL/Complex.thy Fri Sep 03 18:20:13 2021 +0100
@@ -27,6 +27,7 @@
by (auto intro: complex.expand)
+
subsection \<open>Addition and Subtraction\<close>
instantiation complex :: ab_group_add
@@ -655,6 +656,9 @@
subsection \<open>Basic Lemmas\<close>
+lemma complex_of_real_code[code_unfold]: "of_real = (\<lambda>x. Complex x 0)"
+ by (intro ext, auto simp: complex_eq_iff)
+
lemma complex_eq_0: "z=0 \<longleftrightarrow> (Re z)\<^sup>2 + (Im z)\<^sup>2 = 0"
by (metis zero_complex.sel complex_eqI sum_power2_eq_zero_iff)