feat: add Prime.not_dvd_finset_prod and Prime.not_dvd_finsupp_prod (#…

…10047)

We already have `Prime.not_dvd_prod`, which is about list products: https://github.com/leanprover-community/mathlib4/blob/1fec3c4a56a0a991f7324bb7b1f89ab6a6795d19/Mathlib/Data/List/Prime.lean#L41-L43

This PR adds analogous theorems for `Finset` and `Finsupp`.

Mathlib/Algebra/BigOperators/Associated.lean

@@ -201,9 +201,17 @@ theorem Prime.dvd_finset_prod_iff {S : Finset α} {p : M} (pp : Prime p) (g : α
   ⟨pp.exists_mem_finset_dvd, fun ⟨_, ha1, ha2⟩ => dvd_trans ha2 (dvd_prod_of_mem g ha1)⟩
 #align prime.dvd_finset_prod_iff Prime.dvd_finset_prod_iff
 
+theorem Prime.not_dvd_finset_prod {S : Finset α} {p : M} (pp : Prime p) {g : α → M}
+    (hS : ∀ a ∈ S, ¬p ∣ g a) : ¬p ∣ S.prod g := by
+  exact mt (Prime.dvd_finset_prod_iff pp _).1 <| not_exists.2 fun a => not_and.2 (hS a)
+
 theorem 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 _
 #align prime.dvd_finsupp_prod_iff Prime.dvd_finsupp_prod_iff
 
+theorem Prime.not_dvd_finsupp_prod {f : α →₀ M} {g : α → M → ℕ} {p : ℕ} (pp : Prime p)
+    (hS : ∀ a ∈ f.support, ¬p ∣ g a (f a)) : ¬p ∣ f.prod g :=
+  Prime.not_dvd_finset_prod pp hS
+
 end CommMonoidWithZero