src/HOL/Library/Product_plus.thy
changeset 37664 2946b8f057df
parent 36627 39b2516a1970
child 37678 0040bafffdef
     1.1 --- a/src/HOL/Library/Product_plus.thy	Thu Jul 01 08:13:20 2010 +0200
     1.2 +++ b/src/HOL/Library/Product_plus.thy	Thu Jul 01 09:01:09 2010 +0200
     1.3 @@ -118,4 +118,7 @@
     1.4  lemma snd_setsum: "snd (\<Sum>x\<in>A. f x) = (\<Sum>x\<in>A. snd (f x))"
     1.5  by (cases "finite A", induct set: finite, simp_all)
     1.6  
     1.7 +lemma setsum_prod: "(\<Sum>x\<in>A. (f x, g x)) = (\<Sum>x\<in>A. f x, \<Sum>x\<in>A. g x)"
     1.8 +by (cases "finite A", induct set: finite) (simp_all add: zero_prod_def)
     1.9 +
    1.10  end