English
The product of prime factors of n that lie in s is an s-factored number.
Русский
Произведение простых делителей n, входящих в s, является s-факторованным числом.
LaTeX
$$ (n.primeFactorsList.filter (· ∈ s)).prod ∈ factoredNumbers s$$
Lean4
/-- The product of the prime factors of `n` that are in `s` is an `s`-factored number. -/
theorem prod_mem_factoredNumbers (s : Finset ℕ) (n : ℕ) :
(n.primeFactorsList.filter (· ∈ s)).prod ∈ factoredNumbers s :=
by
have h₀ : (n.primeFactorsList.filter (· ∈ s)).prod ≠ 0 :=
List.prod_ne_zero fun h ↦ (pos_of_mem_primeFactorsList (List.mem_of_mem_filter h)).false
refine ⟨h₀, fun p hp ↦ ?_⟩
obtain ⟨H₁, H₂⟩ := (mem_primeFactorsList h₀).mp hp
simpa only [decide_eq_true_eq] using
List.of_mem_filter <|
mem_list_primes_of_dvd_prod H₁.prime
(fun _ hq ↦ (prime_of_mem_primeFactorsList (List.mem_of_mem_filter hq)).prime) H₂
