English
If m is n-smooth and k divides m, then k is n-smooth as well.
Русский
Если m является n-гладким, и k делит m, то k также является n-гладким.
LaTeX
$$$m \in \mathrm{smoothNumbers}(n) \land k \mid m \Rightarrow k \in \mathrm{smoothNumbers}(n)$$$
Lean4
/-- A number that divides an `n`-smooth number is itself `n`-smooth. -/
theorem mem_smoothNumbers_of_dvd {n m k : ℕ} (h : m ∈ smoothNumbers n) (h' : k ∣ m) : k ∈ smoothNumbers n :=
by
simp only [smoothNumbers_eq_factoredNumbers] at h ⊢
exact mem_factoredNumbers_of_dvd h h'