diff -r 00c436488398 -r bdff8bf0a75b src/HOL/Analysis/Euclidean_Space.thy
--- a/src/HOL/Analysis/Euclidean_Space.thy	Tue Feb 20 22:25:23 2018 +0100
+++ b/src/HOL/Analysis/Euclidean_Space.thy	Thu Feb 22 15:17:25 2018 +0100
@@ -84,6 +84,10 @@
 lemma (in euclidean_space) euclidean_representation: "(\<Sum>b\<in>Basis. inner x b *\<^sub>R b) = x"
   unfolding euclidean_representation_sum by simp
 
+lemma (in euclidean_space) euclidean_inner: "inner x y = (\<Sum>b\<in>Basis. (inner x b) * (inner y b))"
+  by (subst (1 2) euclidean_representation [symmetric])
+    (simp add: inner_sum_right inner_Basis ac_simps)
+
 lemma (in euclidean_space) choice_Basis_iff:
   fixes P :: "'a \<Rightarrow> real \<Rightarrow> bool"
   shows "(\<forall>i\<in>Basis. \<exists>x. P i x) \<longleftrightarrow> (\<exists>x. \<forall>i\<in>Basis. P i (inner x i))"