equal
deleted
inserted
replaced
1406 |
1406 |
1407 lemma setprod_nonzero_nat: |
1407 lemma setprod_nonzero_nat: |
1408 "finite A ==> (\<forall>x \<in> A. f x \<noteq> (0::nat)) ==> setprod f A \<noteq> 0" |
1408 "finite A ==> (\<forall>x \<in> A. f x \<noteq> (0::nat)) ==> setprod f A \<noteq> 0" |
1409 by (rule setprod_nonzero, auto) |
1409 by (rule setprod_nonzero, auto) |
1410 |
1410 |
|
1411 lemma setprod_pos_nat: |
|
1412 "finite S ==> (ALL x : S. f x > (0::nat)) ==> setprod f S > 0" |
|
1413 using setprod_nonzero_nat by simp |
|
1414 |
1411 lemma setprod_zero_eq_nat: |
1415 lemma setprod_zero_eq_nat: |
1412 "finite A ==> (setprod f A = (0::nat)) = (\<exists>x \<in> A. f x = 0)" |
1416 "finite A ==> (setprod f A = (0::nat)) = (\<exists>x \<in> A. f x = 0)" |
1413 by (rule setprod_zero_eq, auto) |
1417 by (rule setprod_zero_eq, auto) |
1414 |
1418 |
1415 lemma setprod_nonzero_int: |
1419 lemma setprod_nonzero_int: |