English
Let s be a Finset of M₀ with primes, and n ∈ M₀. If the product over s divides n, then some a ∈ s is prime and divides n.
Русский
Пусть s — конечный набор простых элементов M₀, и n ∈ M₀. Если (s.prod) ∣ n, то найдётся a ∈ s такое, что a ∈ Prime и a ∣ n.
LaTeX
$$s : Finset M₀, ∀ a ∈ s, Prime a → ∀ a ∈ s, a ∣ n → ∃ i ∈ s, semigroupDvd.dvd a n$$
Lean4
theorem prod_primes_dvd [CancelCommMonoidWithZero M₀] [Subsingleton M₀ˣ] {s : Finset M₀} (n : M₀) (h : ∀ a ∈ s, Prime a)
(div : ∀ a ∈ s, a ∣ n) : ∏ p ∈ s, p ∣ n := by
classical
exact
Multiset.prod_primes_dvd n (by simpa only [Multiset.map_id', Finset.mem_def] using h)
(by simpa only [Multiset.map_id', Finset.mem_def] using div)
(by
simp only [Multiset.map_id', associated_eq_eq, Multiset.countP_eq_card_filter, ← s.val.count_eq_card_filter_eq,
← Multiset.nodup_iff_count_le_one, s.nodup])
