src/HOL/Analysis/Bounded_Linear_Function.thy
changeset 66804 3f9bb52082c4
parent 66447 a1f5c5c26fa6
child 66827 c94531b5007d
     1.1 --- a/src/HOL/Analysis/Bounded_Linear_Function.thy	Sun Oct 08 22:28:20 2017 +0200
     1.2 +++ b/src/HOL/Analysis/Bounded_Linear_Function.thy	Sun Oct 08 22:28:20 2017 +0200
     1.3 @@ -387,7 +387,7 @@
     1.4    have "(\<Sum>j\<in>Basis. \<Sum>i\<in>Basis. (x \<bullet> i * (f i \<bullet> j)) *\<^sub>R j) \<bullet> b
     1.5      = (\<Sum>j\<in>Basis. if j = b then (\<Sum>i\<in>Basis. (x \<bullet> i * (f i \<bullet> j))) else 0)"
     1.6      using b
     1.7 -    by (simp add: inner_sum_left inner_Basis if_distrib cong: if_cong) (simp add: sum.commute)
     1.8 +    by (simp add: inner_sum_left inner_Basis if_distrib cong: if_cong) (simp add: sum.swap)
     1.9    also have "\<dots> = (\<Sum>i\<in>Basis. (x \<bullet> i * (f i \<bullet> b)))"
    1.10      using b by (simp add: sum.delta)
    1.11    also have "\<dots> = f x \<bullet> b"