equal
deleted
inserted
replaced
109 |
109 |
110 |
110 |
111 subsection \<open>Properties of Nonstandard Real and Imaginary Parts\<close> |
111 subsection \<open>Properties of Nonstandard Real and Imaginary Parts\<close> |
112 |
112 |
113 lemma hcomplex_hRe_hIm_cancel_iff: "\<And>w z. w = z \<longleftrightarrow> hRe w = hRe z \<and> hIm w = hIm z" |
113 lemma hcomplex_hRe_hIm_cancel_iff: "\<And>w z. w = z \<longleftrightarrow> hRe w = hRe z \<and> hIm w = hIm z" |
114 by transfer (rule complex_Re_Im_cancel_iff) |
114 by transfer (rule complex_eq_iff) |
115 |
115 |
116 lemma hcomplex_equality [intro?]: "\<And>z w. hRe z = hRe w \<Longrightarrow> hIm z = hIm w \<Longrightarrow> z = w" |
116 lemma hcomplex_equality [intro?]: "\<And>z w. hRe z = hRe w \<Longrightarrow> hIm z = hIm w \<Longrightarrow> z = w" |
117 by transfer (rule complex_equality) |
117 by transfer (rule complex_eqI) |
118 |
118 |
119 lemma hcomplex_hRe_zero [simp]: "hRe 0 = 0" |
119 lemma hcomplex_hRe_zero [simp]: "hRe 0 = 0" |
120 by transfer simp |
120 by transfer simp |
121 |
121 |
122 lemma hcomplex_hIm_zero [simp]: "hIm 0 = 0" |
122 lemma hcomplex_hIm_zero [simp]: "hIm 0 = 0" |