src/HOL/Multivariate_Analysis/Linear_Algebra.thy
changeset 56479 91958d4b30f7
parent 56444 f944ae8c80a3
child 56480 093ea91498e6
     1.1 --- a/src/HOL/Multivariate_Analysis/Linear_Algebra.thy	Tue Apr 08 23:16:00 2014 +0200
     1.2 +++ b/src/HOL/Multivariate_Analysis/Linear_Algebra.thy	Wed Apr 09 09:37:47 2014 +0200
     1.3 @@ -1149,7 +1149,7 @@
     1.4        setsum (\<lambda>v. (- (inverse (u ?a))) *\<^sub>R (u v *\<^sub>R v)) S - ?u v *\<^sub>R v"
     1.5        using fS vS uv by (simp add: setsum_diff1 divide_inverse field_simps)
     1.6      also have "\<dots> = ?a"
     1.7 -      unfolding scaleR_right.setsum [symmetric] u using uv by (simp add: divide_minus_left)
     1.8 +      unfolding scaleR_right.setsum [symmetric] u using uv by simp
     1.9      finally have "setsum (\<lambda>v. ?u v *\<^sub>R v) ?S = ?a" .
    1.10      with th0 have ?lhs
    1.11        unfolding dependent_def span_explicit
    1.12 @@ -2143,7 +2143,7 @@
    1.13      case False
    1.14      with span_mul[OF th, of "- 1/ k"]
    1.15      have th1: "f a \<in> span (f ` b)"
    1.16 -      by (auto simp: divide_minus_left)
    1.17 +      by auto
    1.18      from inj_on_image_set_diff[OF "2.prems"(3), of "insert a b " "{a}", symmetric]
    1.19      have tha: "f ` insert a b - f ` {a} = f ` (insert a b - {a})" by blast
    1.20      from "2.prems"(2) [unfolded dependent_def bex_simps(8), rule_format, of "f a"]