--- a/src/HOL/Analysis/Linear_Algebra.thy Tue Feb 20 22:25:23 2018 +0100
+++ b/src/HOL/Analysis/Linear_Algebra.thy Thu Feb 22 15:17:25 2018 +0100
@@ -2987,10 +2987,6 @@
lemma infnorm_le_norm: "infnorm x \<le> norm x"
by (simp add: Basis_le_norm infnorm_Max)
-lemma (in euclidean_space) euclidean_inner: "inner x y = (\<Sum>b\<in>Basis. (x \<bullet> b) * (y \<bullet> b))"
- by (subst (1 2) euclidean_representation [symmetric])
- (simp add: inner_sum_right inner_Basis ac_simps)
-
lemma norm_le_infnorm:
fixes x :: "'a::euclidean_space"
shows "norm x \<le> sqrt DIM('a) * infnorm x"