author nipkow Wed Feb 13 09:50:16 2019 +0100 (6 days ago) changeset 69802 6ec272e153f0 parent 69801 a99a0f5474c5 child 69803 a24865b6262f
removed subsumed lemma
 src/HOL/Analysis/Convex.thy file | annotate | diff | revisions src/HOL/Groups_Big.thy file | annotate | diff | revisions
```     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)"
```