English
If p is prime and p does not divide any element of L, then p does not divide the product L.prod.
Русский
Если p простое и не делит ни один элемент списка L, то p не делит произведение L.prod.
LaTeX
$$$\text{theorem not_dvd_prod } (pp : Prime p) (hL : ∀ a \in L, ¬ p \mid a) : \neg p \mid L.prod$$$
Lean4
theorem not_dvd_prod {p : M} {L : List M} (pp : Prime p) (hL : ∀ a ∈ L, ¬p ∣ a) : ¬p ∣ L.prod :=
mt (Prime.dvd_prod_iff pp).1 <| not_exists.2 fun a => not_and.2 (hL a)