src/HOL/Analysis/Linear_Algebra.thy
changeset 67399 eab6ce8368fa
parent 66804 3f9bb52082c4
child 67443 3abf6a722518
     1.1 --- a/src/HOL/Analysis/Linear_Algebra.thy	Wed Jan 10 15:21:49 2018 +0100
     1.2 +++ b/src/HOL/Analysis/Linear_Algebra.thy	Wed Jan 10 15:25:09 2018 +0100
     1.3 @@ -980,7 +980,7 @@
     1.4        by (intro sum.mono_neutral_cong_left) (auto intro: X)
     1.5      also have "\<dots> = (\<Sum>z\<in>{z. X x z \<noteq> 0}. X x z *\<^sub>R z) + (\<Sum>z\<in>{z. X y z \<noteq> 0}. X y z *\<^sub>R z)"
     1.6        by (auto simp add: scaleR_add_left sum.distrib
     1.7 -               intro!: arg_cong2[where f="op +"]  sum.mono_neutral_cong_right X)
     1.8 +               intro!: arg_cong2[where f="(+)"]  sum.mono_neutral_cong_right X)
     1.9      also have "\<dots> = x + y"
    1.10        by (simp add: X(3)[symmetric])
    1.11      also have "\<dots> = (\<Sum>z | X (x + y) z \<noteq> 0. X (x + y) z *\<^sub>R z)"
    1.12 @@ -1024,7 +1024,7 @@
    1.13      show "g (x + y) = g x + g y"
    1.14        unfolding g_def X_add *
    1.15        by (auto simp add: scaleR_add_left sum.distrib
    1.16 -               intro!: arg_cong2[where f="op +"]  sum.mono_neutral_cong_right X)
    1.17 +               intro!: arg_cong2[where f="(+)"]  sum.mono_neutral_cong_right X)
    1.18    next
    1.19      show "g (r *\<^sub>R x) = r *\<^sub>R g x" for r x
    1.20        by (auto simp add: g_def X_cmult scaleR_sum_right intro!: sum.mono_neutral_cong_left X)
    1.21 @@ -1398,7 +1398,7 @@
    1.22    by (simp add: norm_eq_sqrt_inner)
    1.23  
    1.24  
    1.25 -text\<open>Equality of vectors in terms of @{term "op \<bullet>"} products.\<close>
    1.26 +text\<open>Equality of vectors in terms of @{term "(\<bullet>)"} products.\<close>
    1.27  
    1.28  lemma linear_componentwise:
    1.29    fixes f:: "'a::euclidean_space \<Rightarrow> 'b::real_inner"