| changeset 44902 | 9ba11d41cd1f |
| parent 44846 | e9d1fcbc7d20 |
| child 47108 | 2a1953f0d20d |
--- a/src/HOL/Complex.thy Mon Sep 12 09:57:33 2011 -0400 +++ b/src/HOL/Complex.thy Mon Sep 12 09:21:01 2011 -0700 @@ -412,6 +412,9 @@ lemma Complex_eq_i [simp]: "(Complex x y = ii) = (x = 0 \<and> y = 1)" by (simp add: i_def) +lemma norm_ii [simp]: "norm ii = 1" + by (simp add: i_def) + lemma complex_i_not_zero [simp]: "ii \<noteq> 0" by (simp add: complex_eq_iff)