--- a/src/HOL/Analysis/Euclidean_Space.thy Tue Jan 03 23:21:09 2017 +0100
+++ b/src/HOL/Analysis/Euclidean_Space.thy Wed Jan 04 16:18:50 2017 +0000
@@ -53,6 +53,9 @@
lemma (in euclidean_space) SOME_Basis: "(SOME i. i \<in> Basis) \<in> Basis"
by (metis ex_in_conv nonempty_Basis someI_ex)
+lemma norm_some_Basis [simp]: "norm (SOME i. i \<in> Basis) = 1"
+ by (simp add: SOME_Basis)
+
lemma (in euclidean_space) inner_sum_left_Basis[simp]:
"b \<in> Basis \<Longrightarrow> inner (\<Sum>i\<in>Basis. f i *\<^sub>R i) b = f b"
by (simp add: inner_sum_left inner_Basis if_distrib comm_monoid_add_class.sum.If_cases)