smoothNumbers_eq_factoredNumbers_primesBelow

English

The set of n-smooth numbers equals the factoredNumbers of primes below n.

Русский

Множество n-гладких чисел равно факторированию по(primesBelow n).

LaTeX

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

Lean4

/-- The `n`-smooth numbers agree with the `primesBelow n`-factored numbers. -/
theorem smoothNumbers_eq_factoredNumbers_primesBelow (n : ℕ) : smoothNumbers n = factoredNumbers n.primesBelow :=
  by
  rw [smoothNumbers_eq_factoredNumbers]
  refine Set.Subset.antisymm (fun m hm ↦ ?_) <| factoredNumbers_mono Finset.mem_of_mem_filter
  simp_rw [mem_factoredNumbers'] at hm ⊢
  exact fun p hp hp' ↦ mem_primesBelow.mpr ⟨Finset.mem_range.mp <| hm p hp hp', hp⟩

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