removed subsumed lemma
authornipkow
Wed Feb 13 09:50:16 2019 +0100 (2 months ago)
changeset 698026ec272e153f0
parent 69801 a99a0f5474c5
child 69803 a24865b6262f
removed subsumed lemma
src/HOL/Analysis/Convex.thy
src/HOL/Groups_Big.thy
     1.1 --- a/src/HOL/Analysis/Convex.thy	Wed Feb 13 07:48:42 2019 +0100
     1.2 +++ b/src/HOL/Analysis/Convex.thy	Wed Feb 13 09:50:16 2019 +0100
     1.3 @@ -1203,7 +1203,7 @@
     1.4          have c: "card (S - {x}) = card S - 1"
     1.5            by (simp add: Suc.prems(3) \<open>x \<in> S\<close>)
     1.6          have "sum u (S - {x}) = 1 - u x"
     1.7 -          by (simp add: Suc.prems sum_diff1_ring \<open>x \<in> S\<close>)
     1.8 +          by (simp add: Suc.prems sum_diff1 \<open>x \<in> S\<close>)
     1.9          with x have eq1: "inverse (1 - u x) * sum u (S - {x}) = 1"
    1.10            by auto
    1.11          have inV: "(\<Sum>y\<in>S - {x}. (inverse (1 - u x) * u y) *\<^sub>R y) \<in> V"
     2.1 --- a/src/HOL/Groups_Big.thy	Wed Feb 13 07:48:42 2019 +0100
     2.2 +++ b/src/HOL/Groups_Big.thy	Wed Feb 13 09:50:16 2019 +0100
     2.3 @@ -848,12 +848,6 @@
     2.4    finally show ?case .
     2.5  qed
     2.6  
     2.7 -lemma sum_diff1_ring:
     2.8 -  fixes f :: "'b \<Rightarrow> 'a::ring"
     2.9 -  assumes "finite A" "a \<in> A"
    2.10 -  shows "sum f (A - {a}) = sum f A - (f a)"
    2.11 -  unfolding sum.remove [OF assms] by auto
    2.12 -
    2.13  lemma sum_product:
    2.14    fixes f :: "'a \<Rightarrow> 'b::semiring_0"
    2.15    shows "sum f A * sum g B = (\<Sum>i\<in>A. \<Sum>j\<in>B. f i * g j)"