English
If s is a finite set of natural numbers and every element of s is prime, then primeFactors( product of p in s ) equals s.
Русский
Пусть s — конечное множество натуральных чисел, и каждый элемент множества является простым. Тогда primeFactors( произведение элементов s ) равняется s.
LaTeX
$$$\\\\forall s \\\\,(\\\\forall p \\\\in s, p.\\\\Prime) \\\\Rightarrow \\\\operatorname{primeFactors}\\left(\\\\prod_{p \\in s} p\\right) = s.$$$
Lean4
theorem primeFactors_prod (hs : ∀ p ∈ s, p.Prime) : primeFactors (∏ p ∈ s, p) = s :=
by
have hn : ∏ p ∈ s, p ≠ 0 := prod_ne_zero_iff.2 fun p hp ↦ (hs _ hp).ne_zero
ext p
rw [mem_primeFactors_of_ne_zero hn, and_congr_right (fun hp ↦ hp.prime.dvd_finset_prod_iff _)]
refine ⟨?_, fun hp ↦ ⟨hs _ hp, _, hp, dvd_rfl⟩⟩
rintro ⟨hp, q, hq, hpq⟩
rwa [← ((hs _ hq).dvd_iff_eq hp.ne_one).1 hpq]
