src/HOL/Library/Inner_Product.thy
changeset 44902 9ba11d41cd1f
parent 44282 f0de18b62d63
child 49962 a8cc904a6820
     1.1 --- a/src/HOL/Library/Inner_Product.thy	Mon Sep 12 09:57:33 2011 -0400
     1.2 +++ b/src/HOL/Library/Inner_Product.thy	Mon Sep 12 09:21:01 2011 -0700
     1.3 @@ -240,6 +240,18 @@
     1.4  
     1.5  end
     1.6  
     1.7 +lemma complex_inner_1 [simp]: "inner 1 x = Re x"
     1.8 +  unfolding inner_complex_def by simp
     1.9 +
    1.10 +lemma complex_inner_1_right [simp]: "inner x 1 = Re x"
    1.11 +  unfolding inner_complex_def by simp
    1.12 +
    1.13 +lemma complex_inner_ii_left [simp]: "inner ii x = Im x"
    1.14 +  unfolding inner_complex_def by simp
    1.15 +
    1.16 +lemma complex_inner_ii_right [simp]: "inner x ii = Im x"
    1.17 +  unfolding inner_complex_def by simp
    1.18 +
    1.19  
    1.20  subsection {* Gradient derivative *}
    1.21