equal
deleted
inserted
replaced
204 |
204 |
205 lemma hIm_hcomplex_of_hypreal [simp]: "!!z. hIm(hcomplex_of_hypreal z) = 0" |
205 lemma hIm_hcomplex_of_hypreal [simp]: "!!z. hIm(hcomplex_of_hypreal z) = 0" |
206 by transfer (rule Im_complex_of_real) |
206 by transfer (rule Im_complex_of_real) |
207 |
207 |
208 lemma hcomplex_of_hypreal_epsilon_not_zero [simp]: |
208 lemma hcomplex_of_hypreal_epsilon_not_zero [simp]: |
209 "hcomplex_of_hypreal epsilon \<noteq> 0" |
209 "hcomplex_of_hypreal \<epsilon> \<noteq> 0" |
210 by (simp add: hypreal_epsilon_not_zero) |
210 by (simp add: hypreal_epsilon_not_zero) |
211 |
211 |
212 subsection\<open>HComplex theorems\<close> |
212 subsection\<open>HComplex theorems\<close> |
213 |
213 |
214 lemma hRe_HComplex [simp]: "!!x y. hRe (HComplex x y) = x" |
214 lemma hRe_HComplex [simp]: "!!x y. hRe (HComplex x y) = x" |