feat(algebra/big_operators/associated): dvd_prod_iff for finset and finsupp (#10675)

Adding the counterparts of `dvd_prod_iff` (in #10624) for `finset` and `finsupp`.

Author: stuart-presnell

src/algebra/big_operators/associated.lean

@@ -6,12 +6,13 @@ Authors: Johannes Hölzl, Jens Wagemaker, Anne Baanen
 
 import algebra.associated
 import algebra.big_operators.basic
+import data.finsupp.basic
 
 /-!
 # Products of associated, prime, and irreducible elements.
 
 This file contains some theorems relating definitions in `algebra.associated`
-and products of multisets and finsets.
+and products of multisets, finsets, and finsupps.
 
 -/
 
@@ -120,8 +121,22 @@ multiset.prod_ne_zero (λ h0, prime.ne_zero (h 0 h0) rfl)
 
 end multiset
 
+open finset finsupp
+
+section comm_monoid_with_zero
+
+variables {M : Type*} [comm_monoid_with_zero M]
+
+lemma prime.dvd_finset_prod_iff {S : finset α} {p : M} (pp : prime p) (g : α → M) :
+  p ∣ S.prod g ↔ ∃ a ∈ S, p ∣ g a :=
+⟨pp.exists_mem_finset_dvd, λ ⟨a, ha1, ha2⟩, dvd_trans ha2 (dvd_prod_of_mem g ha1)⟩
+
+lemma prime.dvd_finsupp_prod_iff  {f: α →₀ M} {g : α → M → ℕ} {p : ℕ} (pp : prime p) :
+  p ∣ f.prod g ↔ ∃ a ∈ f.support, p ∣ g a (f a) :=
+prime.dvd_finset_prod_iff pp _
+
 /-- Prime `p` divides the product of a list `L` iff it divides some `a ∈ L` -/
-lemma prime.dvd_prod_iff {M : Type*} [comm_monoid_with_zero M] {p : M} {L : list M} (pp : prime p) :
+lemma prime.dvd_prod_iff {p : M} {L : list M} (pp : prime p) :
 p ∣ L.prod ↔ ∃ a ∈ L, p ∣ a :=
 begin
   split,
@@ -133,3 +148,14 @@ begin
       { rcases L_ih h_1 with ⟨x, hx1, hx2⟩, use x, simp [list.mem_cons_iff, hx1, hx2] } } },
   { exact λ ⟨a, ha1, ha2⟩, dvd_trans ha2 (list.dvd_prod ha1) },
 end
+
+end comm_monoid_with_zero
+
+lemma nat.prime.dvd_finset_prod_iff {α : Type*} {S : finset α} {p : ℕ}
+  (pp : prime p) (g : α → ℕ) : p ∣ S.prod g ↔ ∃ a ∈ S, p ∣ g a :=
+by apply prime.dvd_finset_prod_iff pp
+
+lemma nat.prime.dvd_finsupp_prod_iff {α M : Type*} [has_zero M] {f: α →₀ M}
+  {g : α → M → ℕ} {p : ℕ} (pp : prime p) :
+p ∣ f.prod g ↔ ∃ a ∈ f.support, p ∣ g a (f a) :=
+nat.prime.dvd_finset_prod_iff pp _