equal
deleted
inserted
replaced
23 lemma complex_eqI [intro?]: "Re x = Re y \<Longrightarrow> Im x = Im y \<Longrightarrow> x = y" |
23 lemma complex_eqI [intro?]: "Re x = Re y \<Longrightarrow> Im x = Im y \<Longrightarrow> x = y" |
24 by (rule complex.expand) simp |
24 by (rule complex.expand) simp |
25 |
25 |
26 lemma complex_eq_iff: "x = y \<longleftrightarrow> Re x = Re y \<and> Im x = Im y" |
26 lemma complex_eq_iff: "x = y \<longleftrightarrow> Re x = Re y \<and> Im x = Im y" |
27 by (auto intro: complex.expand) |
27 by (auto intro: complex.expand) |
28 |
|
29 |
|
30 |
28 |
31 subsection \<open>Addition and Subtraction\<close> |
29 subsection \<open>Addition and Subtraction\<close> |
32 |
30 |
33 instantiation complex :: ab_group_add |
31 instantiation complex :: ab_group_add |
34 begin |
32 begin |