equal
deleted
inserted
replaced
159 lemma hIm_minus: "!!z. hIm(-z) = - hIm(z)" |
159 lemma hIm_minus: "!!z. hIm(-z) = - hIm(z)" |
160 by transfer (rule complex_Im_minus) |
160 by transfer (rule complex_Im_minus) |
161 |
161 |
162 lemma hcomplex_add_minus_eq_minus: |
162 lemma hcomplex_add_minus_eq_minus: |
163 "x + y = (0::hcomplex) ==> x = -y" |
163 "x + y = (0::hcomplex) ==> x = -y" |
164 apply (drule OrderedGroup.equals_zero_I) |
164 apply (drule OrderedGroup.minus_unique) |
165 apply (simp add: minus_equation_iff [of x y]) |
165 apply (simp add: minus_equation_iff [of x y]) |
166 done |
166 done |
167 |
167 |
168 lemma hcomplex_i_mult_eq [simp]: "iii * iii = - 1" |
168 lemma hcomplex_i_mult_eq [simp]: "iii * iii = - 1" |
169 by transfer (rule i_mult_eq2) |
169 by transfer (rule i_mult_eq2) |