English
A k-smooth number n can be written as n = m^2 · (P), where P is a product of distinct primes < k; equivalently, there exists s ∈ k.primesBelow.powerset with n = m^2 · (s.prod id).
Русский
Каждое k-гладкое число n можно записать как n = m^2 · P, где P — произведение различных простых меньше чем k; эквивалентно существованию s ∈ k.primesBelow.powerset такое, что n = m^2 · (s.prod id).
LaTeX
$$$\forall n\in \mathrm{smoothNumbers}(k),\; \exists s \in k.primesBelow.powerset,\; \exists m,\ n = m^2 \cdot (s.prod\ id)$$$
Lean4
/-- A `k`-smooth number can be written as a square times a product of distinct primes `< k`. -/
theorem eq_prod_primes_mul_sq_of_mem_smoothNumbers {n k : ℕ} (h : n ∈ smoothNumbers k) :
∃ s ∈ k.primesBelow.powerset, ∃ m, n = m ^ 2 * (s.prod id) :=
by
obtain ⟨l, m, H₁, H₂⟩ := sq_mul_squarefree n
have hl : l ∈ smoothNumbers k := mem_smoothNumbers_of_dvd h (Dvd.intro_left (m ^ 2) H₁)
refine ⟨l.primeFactorsList.toFinset, ?_, m, ?_⟩
· simp only [toFinset_factors, Finset.mem_powerset]
refine fun p hp ↦ mem_primesBelow.mpr ⟨?_, (mem_primeFactors.mp hp).1⟩
rw [mem_primeFactors] at hp
exact mem_smoothNumbers'.mp hl p hp.1 hp.2.1
rw [← H₁]
congr
simp only [toFinset_factors]
exact (prod_primeFactors_of_squarefree H₂).symm
