not_dvd_prod — Mathlib

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)

Похожие утверждения