equal
deleted
inserted
replaced
50 lemma (in euclidean_space) inner_not_same_Basis: "u \<in> Basis \<Longrightarrow> v \<in> Basis \<Longrightarrow> u \<noteq> v \<Longrightarrow> inner u v = 0" |
50 lemma (in euclidean_space) inner_not_same_Basis: "u \<in> Basis \<Longrightarrow> v \<in> Basis \<Longrightarrow> u \<noteq> v \<Longrightarrow> inner u v = 0" |
51 by (simp add: inner_Basis) |
51 by (simp add: inner_Basis) |
52 |
52 |
53 lemma (in euclidean_space) sgn_Basis: "u \<in> Basis \<Longrightarrow> sgn u = u" |
53 lemma (in euclidean_space) sgn_Basis: "u \<in> Basis \<Longrightarrow> sgn u = u" |
54 unfolding sgn_div_norm by (simp add: scaleR_one) |
54 unfolding sgn_div_norm by (simp add: scaleR_one) |
|
55 |
|
56 lemma inner_sum_Basis[simp]: "i \<in> Basis \<Longrightarrow> inner (\<Sum>Basis) i = 1" |
|
57 by (simp add: inner_sum_left sum.If_cases inner_Basis) |
55 |
58 |
56 lemma (in euclidean_space) Basis_zero [simp]: "0 \<notin> Basis" |
59 lemma (in euclidean_space) Basis_zero [simp]: "0 \<notin> Basis" |
57 proof |
60 proof |
58 assume "0 \<in> Basis" thus "False" |
61 assume "0 \<in> Basis" thus "False" |
59 using inner_Basis [of 0 0] by simp |
62 using inner_Basis [of 0 0] by simp |