1136 |
1136 |
1137 lemma setprod_eq_1_iff [simp]: |
1137 lemma setprod_eq_1_iff [simp]: |
1138 "finite F ==> (setprod f F = 1) = (ALL a:F. f a = (1::nat))" |
1138 "finite F ==> (setprod f F = 1) = (ALL a:F. f a = (1::nat))" |
1139 by (induct set: Finites) auto |
1139 by (induct set: Finites) auto |
1140 |
1140 |
1141 lemma setprod_constant: "finite A ==> (\<Prod>x: A. (y::'a::ringpower)) = |
1141 lemma setprod_constant: "finite A ==> (\<Prod>x: A. (y::'a::recpower)) = y^(card A)" |
1142 y^(card A)" |
|
1143 apply (erule finite_induct) |
1142 apply (erule finite_induct) |
1144 apply (auto simp add: power_Suc) |
1143 apply (auto simp add: power_Suc) |
1145 done |
1144 done |
1146 |
1145 |
1147 lemma setprod_zero: "finite A ==> EX x: A. f x = (0::'a::comm_semiring_1_cancel) ==> |
1146 lemma setprod_zero: |
1148 setprod f A = 0" |
1147 "finite A ==> EX x: A. f x = (0::'a::comm_semiring_1_cancel) ==> setprod f A = 0" |
1149 apply (induct set: Finites, force, clarsimp) |
1148 apply (induct set: Finites, force, clarsimp) |
1150 apply (erule disjE, auto) |
1149 apply (erule disjE, auto) |
1151 done |
1150 done |
1152 |
1151 |
1153 lemma setprod_nonneg [rule_format]: "(ALL x: A. (0::'a::ordered_idom) \<le> f x) |
1152 lemma setprod_nonneg [rule_format]: |
1154 --> 0 \<le> setprod f A" |
1153 "(ALL x: A. (0::'a::ordered_idom) \<le> f x) --> 0 \<le> setprod f A" |
1155 apply (case_tac "finite A") |
1154 apply (case_tac "finite A") |
1156 apply (induct set: Finites, force, clarsimp) |
1155 apply (induct set: Finites, force, clarsimp) |
1157 apply (subgoal_tac "0 * 0 \<le> f x * setprod f F", force) |
1156 apply (subgoal_tac "0 * 0 \<le> f x * setprod f F", force) |
1158 apply (rule mult_mono, assumption+) |
1157 apply (rule mult_mono, assumption+) |
1159 apply (auto simp add: setprod_def) |
1158 apply (auto simp add: setprod_def) |