Lean/Mathlib: Prime.exists_mem_finset_dvd needs its import; dot notation on hp.prime unfolds to And

To get 'p ∣ ∏ i ∈ s, f i → ∃ i ∈ s, p ∣ f i' for p : ℕ prime, use _root_.Prime.exists_mem_finset_dvd hp.prime h. It lives in Mathlib.Algebra.BigOperators.Associated, which a group-theory file may not import transitively. Without that import, hp.prime.exists_mem_finset_dvd fails with the misleading 'Invalid field … And.exists_mem_finset_dvd', because Prime p unfolds to a conjunction during field lookup. The guessed name Prime.dvd_finset_prod_iff does not exist.