src/HOL/Analysis/Linear_Algebra.thy
changeset 63918 6bf55e6e0b75
parent 63886 685fb01256af
child 63938 f6ce08859d4c
     1.1 --- a/src/HOL/Analysis/Linear_Algebra.thy	Mon Sep 19 12:53:30 2016 +0200
     1.2 +++ b/src/HOL/Analysis/Linear_Algebra.thy	Mon Sep 19 20:06:21 2016 +0200
     1.3 @@ -1960,7 +1960,7 @@
     1.4      qed
     1.5      from setsum_norm_le[of _ ?g, OF th]
     1.6      show "norm (f x) \<le> ?B * norm x"
     1.7 -      unfolding th0 setsum_left_distrib by metis
     1.8 +      unfolding th0 setsum_distrib_right by metis
     1.9    qed
    1.10  qed
    1.11  
    1.12 @@ -2021,7 +2021,7 @@
    1.13      unfolding bilinear_setsum[OF bh finite_Basis finite_Basis] ..
    1.14    finally have th: "norm (h x y) = \<dots>" .
    1.15    show "norm (h x y) \<le> (\<Sum>i\<in>Basis. \<Sum>j\<in>Basis. norm (h i j)) * norm x * norm y"
    1.16 -    apply (auto simp add: setsum_left_distrib th setsum.cartesian_product)
    1.17 +    apply (auto simp add: setsum_distrib_right th setsum.cartesian_product)
    1.18      apply (rule setsum_norm_le)
    1.19      apply simp
    1.20      apply (auto simp add: bilinear_rmul[OF bh] bilinear_lmul[OF bh]