equal
deleted
inserted
replaced
229 |
229 |
230 subsection{* Properties of Embedding from Reals *} |
230 subsection{* Properties of Embedding from Reals *} |
231 |
231 |
232 abbreviation complex_of_real :: "real \<Rightarrow> complex" |
232 abbreviation complex_of_real :: "real \<Rightarrow> complex" |
233 where "complex_of_real \<equiv> of_real" |
233 where "complex_of_real \<equiv> of_real" |
|
234 |
|
235 declare [[coercion complex_of_real]] |
234 |
236 |
235 lemma complex_of_real_def: "complex_of_real r = Complex r 0" |
237 lemma complex_of_real_def: "complex_of_real r = Complex r 0" |
236 by (simp add: of_real_def complex_scaleR_def) |
238 by (simp add: of_real_def complex_scaleR_def) |
237 |
239 |
238 lemma Re_complex_of_real [simp]: "Re (complex_of_real z) = z" |
240 lemma Re_complex_of_real [simp]: "Re (complex_of_real z) = z" |