smoothNumbers_succ — Mathlib

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]

Похожие утверждения