English
For a prime p and a list L, p divides the product L.prod if and only if p divides some element a of L.
Русский
Для простого p и списка L верно: p делит произведение L.prod тогда и только тогда, когда p делит некоторый элемент a из L.
LaTeX
$$$\text{theorem } dvd\_prod\_iff (pp : Prime p) : p \mid L.prod \leftrightarrow \exists a \in L, p \mid a$$$
Lean4
/-- Prime `p` divides the product of a list `L` iff it divides some `a ∈ L` -/
theorem dvd_prod_iff {p : M} {L : List M} (pp : Prime p) : p ∣ L.prod ↔ ∃ a ∈ L, p ∣ a :=
by
constructor
· intro h
induction L with
| nil =>
rw [prod_nil] at h
exact absurd h pp.not_dvd_one
| cons L_hd L_tl L_ih =>
rw [prod_cons] at h
rcases pp.dvd_or_dvd h with hd | hd
· exact ⟨L_hd, mem_cons_self, hd⟩
· obtain ⟨x, hx1, hx2⟩ := L_ih hd
exact ⟨x, mem_cons_of_mem L_hd hx1, hx2⟩
· exact fun ⟨a, ha1, ha2⟩ => dvd_trans ha2 (dvd_prod ha1)
