src/HOL/Finite_Set.thy
changeset 34223 dce32a1e05fe
parent 34114 f3fd41b9c017
child 35028 108662d50512
     1.1 --- a/src/HOL/Finite_Set.thy	Fri Jan 01 17:21:44 2010 +0100
     1.2 +++ b/src/HOL/Finite_Set.thy	Fri Jan 01 19:15:43 2010 +0100
     1.3 @@ -1737,6 +1737,13 @@
     1.4    shows "setsum f A * setsum g B = (\<Sum>i\<in>A. \<Sum>j\<in>B. f i * g j)"
     1.5    by (simp add: setsum_right_distrib setsum_left_distrib) (rule setsum_commute)
     1.6  
     1.7 +lemma setsum_mult_setsum_if_inj:
     1.8 +fixes f :: "'a => ('b::semiring_0)"
     1.9 +shows "inj_on (%(a,b). f a * g b) (A \<times> B) ==>
    1.10 +  setsum f A * setsum g B = setsum id {f a * g b|a b. a:A & b:B}"
    1.11 +by(auto simp: setsum_product setsum_cartesian_product
    1.12 +        intro!:  setsum_reindex_cong[symmetric])
    1.13 +
    1.14  
    1.15  subsection {* Generalized product over a set *}
    1.16