src/HOL/Complex.thy
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)