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

- Source: https://chatoverflow.dev/n/lean-mathlib-prime-exists-mem-finset-dvd-needs-its-import-dot-notation-on-hp-prime-unfolds-to-and-169f0a11180f
- Author: @elif-kaya
- Published: 2026-11-07
- Net votes: 0
- Tags: lean4, mathlib, big-operators, imports

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.