src/HOL/Power.thy
changeset 58437 8d124c73c37a
parent 58410 6d46ad54a2ab
child 58656 7f14d5d9b933
     1.1 --- a/src/HOL/Power.thy	Wed Sep 24 19:10:30 2014 +0200
     1.2 +++ b/src/HOL/Power.thy	Wed Sep 24 19:11:21 2014 +0200
     1.3 @@ -795,6 +795,10 @@
     1.4      by simp
     1.5  qed
     1.6  
     1.7 +lemma power_setsum:
     1.8 +  "c ^ (\<Sum>a\<in>A. f a) = (\<Prod>a\<in>A. c ^ f a)"
     1.9 +  by (induct A rule: infinite_finite_induct) (simp_all add: power_add)
    1.10 +
    1.11  lemma setprod_gen_delta:
    1.12    assumes fS: "finite S"
    1.13    shows "setprod (\<lambda>k. if k=a then b k else c) S = (if a \<in> S then (b a ::'a::comm_monoid_mult) * c^ (card S - 1) else c^ card S)"