equal
deleted
inserted
replaced
792 by (induct A rule: finite_induct) (auto simp add: power_mult_distrib) |
792 by (induct A rule: finite_induct) (auto simp add: power_mult_distrib) |
793 next |
793 next |
794 case False then show ?thesis |
794 case False then show ?thesis |
795 by simp |
795 by simp |
796 qed |
796 qed |
|
797 |
|
798 lemma power_setsum: |
|
799 "c ^ (\<Sum>a\<in>A. f a) = (\<Prod>a\<in>A. c ^ f a)" |
|
800 by (induct A rule: infinite_finite_induct) (simp_all add: power_add) |
797 |
801 |
798 lemma setprod_gen_delta: |
802 lemma setprod_gen_delta: |
799 assumes fS: "finite S" |
803 assumes fS: "finite S" |
800 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)" |
804 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)" |
801 proof- |
805 proof- |