English
Let p be a prime element of a commutative monoid with zero M₀. For any multiset s of M₀, if p divides the product s.prod, then there exists a ∈ s such that p divides a.
Русский
Пусть p — простое элемент в коммутативной моноиде с нулём M₀. Для любого мультисета s в M₀, если p делит произведение s.prod, то существует a ∈ s такое, что p делит a.
LaTeX
$$$p$ is prime in $M_0$ and $s$ is a multiset of $M_0$. If $p \\mid s.\\mathrm{prod}$, then $\\exists a \\in s$ with $p \\mid a$.$$
Lean4
theorem exists_mem_multiset_dvd (hp : Prime p) {s : Multiset M₀} : p ∣ s.prod → ∃ a ∈ s, p ∣ a :=
Multiset.induction_on s (fun h => (hp.not_dvd_one h).elim) fun a s ih h =>
have : p ∣ a * s.prod := by simpa using h
match hp.dvd_or_dvd this with
| Or.inl h => ⟨a, Multiset.mem_cons_self a s, h⟩
| Or.inr h =>
let ⟨a, has, h⟩ := ih h
⟨a, Multiset.mem_cons_of_mem has, h⟩
