src/HOL/Analysis/Linear_Algebra.thy
changeset 67685 bdff8bf0a75b
parent 67443 3abf6a722518
child 67962 0acdcd8f4ba1
     1.1 --- a/src/HOL/Analysis/Linear_Algebra.thy	Tue Feb 20 22:25:23 2018 +0100
     1.2 +++ b/src/HOL/Analysis/Linear_Algebra.thy	Thu Feb 22 15:17:25 2018 +0100
     1.3 @@ -2987,10 +2987,6 @@
     1.4  lemma infnorm_le_norm: "infnorm x \<le> norm x"
     1.5    by (simp add: Basis_le_norm infnorm_Max)
     1.6  
     1.7 -lemma (in euclidean_space) euclidean_inner: "inner x y = (\<Sum>b\<in>Basis. (x \<bullet> b) * (y \<bullet> b))"
     1.8 -  by (subst (1 2) euclidean_representation [symmetric])
     1.9 -    (simp add: inner_sum_right inner_Basis ac_simps)
    1.10 -
    1.11  lemma norm_le_infnorm:
    1.12    fixes x :: "'a::euclidean_space"
    1.13    shows "norm x \<le> sqrt DIM('a) * infnorm x"