--- a/src/HOL/Finite_Set.thy Fri Mar 17 09:57:25 2006 +0100
+++ b/src/HOL/Finite_Set.thy Fri Mar 17 10:04:27 2006 +0100
@@ -1145,10 +1145,7 @@
apply auto
done
-(* FIXME: this is distributitivty, name as such! *)
-(* suggested name: setsum_right_distrib (CB) *)
-
-lemma setsum_mult:
+lemma setsum_right_distrib:
fixes f :: "'a => ('b::semiring_0_cancel)"
shows "r * setsum f A = setsum (%n. r * f n) A"
proof (cases "finite A")
@@ -1270,6 +1267,11 @@
finally show "?s = ?t" .
qed
+lemma setsum_product:
+ fixes f :: "nat => ('a::semiring_0_cancel)"
+ shows "setsum f A * setsum g B = (\<Sum>i\<in>A. \<Sum>j\<in>B. f i * g j)"
+ by (simp add: setsum_right_distrib setsum_left_distrib) (rule setsum_commute)
+
subsection {* Generalized product over a set *}