src/HOL/Groups_Big.thy
changeset 58349 107341a15946
parent 58195 1fee63e0377d
child 58437 8d124c73c37a
     1.1 --- a/src/HOL/Groups_Big.thy	Tue Sep 16 16:04:08 2014 +0200
     1.2 +++ b/src/HOL/Groups_Big.thy	Tue Sep 16 18:42:33 2014 +0200
     1.3 @@ -948,6 +948,9 @@
     1.4  apply (auto simp add: algebra_simps)
     1.5  done
     1.6  
     1.7 +lemma setsum_Suc: "setsum (%x. Suc(f x)) A = setsum f A + card A"
     1.8 +using setsum.distrib[of f "%_. 1" A] by(simp)
     1.9 +
    1.10  lemma setsum_bounded:
    1.11    assumes le: "\<And>i. i\<in>A \<Longrightarrow> f i \<le> (K::'a::{semiring_1, ordered_ab_semigroup_add})"
    1.12    shows "setsum f A \<le> of_nat (card A) * K"