src/HOL/Analysis/Linear_Algebra.thy
changeset 69510 0f31dd2e540d
parent 68901 4824cc40f42e
child 69513 42e08052dae8
     1.1 --- a/src/HOL/Analysis/Linear_Algebra.thy	Thu Dec 27 19:48:41 2018 +0100
     1.2 +++ b/src/HOL/Analysis/Linear_Algebra.thy	Thu Dec 27 21:00:50 2018 +0100
     1.3 @@ -106,12 +106,6 @@
     1.4    using sum_norm_le[OF K] sum_constant[symmetric]
     1.5    by simp
     1.6  
     1.7 -lemma sum_group:
     1.8 -  assumes fS: "finite S" and fT: "finite T" and fST: "f ` S \<subseteq> T"
     1.9 -  shows "sum (\<lambda>y. sum g {x. x \<in> S \<and> f x = y}) T = sum g S"
    1.10 -  unfolding sum_image_gen[OF fS, of g f]
    1.11 -  by (auto intro: sum.neutral sum.mono_neutral_right[OF fT fST])
    1.12 -
    1.13  lemma vector_eq_ldot: "(\<forall>x. x \<bullet> y = x \<bullet> z) \<longleftrightarrow> y = z"
    1.14  proof
    1.15    assume "\<forall>x. x \<bullet> y = x \<bullet> z"