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