English
If m is n-smooth and k divides m, then k is n-smooth.
Русский
Если m ∈ n-smooth и k делит m, то k ∈ n-smooth.
LaTeX
$$$m \in \mathrm{smoothNumbers}(n) \land k \mid m \Rightarrow k \in \mathrm{smoothNumbers}(n)$$$
Lean4
/-- The sets of `N`-smooth and of `(N+1)`-smooth numbers are the same when `N` is not prime.
See `Nat.equivProdNatSmoothNumbers` for when `N` is prime. -/
theorem smoothNumbers_succ {N : ℕ} (hN : ¬N.Prime) : (N + 1).smoothNumbers = N.smoothNumbers := by
simp only [smoothNumbers_eq_factoredNumbers, Finset.range_add_one, factoredNumbers_insert _ hN]