smoothNumbers_eq_factoredNumbers — Mathlib

English

The set of n-smooth numbers is exactly the set of numbers factored from Finset.range n.

Русский

Множество n-гладких чисел совпадает с множеством факторированных чисел Finset.range n.

LaTeX

$$$\mathrm{smoothNumbers}(n) = \mathrm{factoredNumbers}(\mathrm{Finset.range}(n))$$$

Lean4

/-- The `n`-smooth numbers agree with the `Finset.range n`-factored numbers. -/
theorem smoothNumbers_eq_factoredNumbers (n : ℕ) : smoothNumbers n = factoredNumbers (Finset.range n) := by
  simp only [smoothNumbers, ne_eq, mem_primeFactorsList', and_imp, factoredNumbers, Finset.mem_range]

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