equal
deleted
inserted
replaced
573 qed |
573 qed |
574 |
574 |
575 lemma nproduct_cmul: |
575 lemma nproduct_cmul: |
576 assumes fS:"finite S" |
576 assumes fS:"finite S" |
577 shows "setprod (\<lambda>m. (c::'a::{comm_monoid_mult})* a(m)) S = c ^ (card S) * setprod a S" |
577 shows "setprod (\<lambda>m. (c::'a::{comm_monoid_mult})* a(m)) S = c ^ (card S) * setprod a S" |
578 unfolding setprod_timesf setprod_constant[OF fS, of c] .. |
578 unfolding setprod.distrib setprod_constant[OF fS, of c] .. |
579 |
579 |
580 lemma coprime_nproduct: |
580 lemma coprime_nproduct: |
581 assumes fS: "finite S" and Sn: "\<forall>x\<in>S. coprime n (a x)" |
581 assumes fS: "finite S" and Sn: "\<forall>x\<in>S. coprime n (a x)" |
582 shows "coprime n (setprod a S)" |
582 shows "coprime n (setprod a S)" |
583 using fS by (rule finite_subset_induct) |
583 using fS by (rule finite_subset_induct) |