mem_smoothNumbers_of_primeFactors_subset

English

An n-smooth number m with primeFactors within Finset.range(n) belongs to n.smoothNumbers.

Русский

Число m с m.primeFactors ⊆ Finset.range(n) и m ≠ 0 принадлежит n.smoothNumbers.

LaTeX

$$$m \neq 0 \wedge m.\text{primeFactors} \subseteq \mathrm{Finset.range}(n) \Rightarrow m \in n.\text{smoothNumbers}$$$

Lean4

/-- `m` is an `n`-smooth number if the `Finset` of its prime factors consists of numbers `< n`. -/
theorem mem_smoothNumbers_of_primeFactors_subset {m n : ℕ} (hm : m ≠ 0) (hp : m.primeFactors ⊆ Finset.range n) :
    m ∈ n.smoothNumbers :=
  smoothNumbers_eq_factoredNumbers n ▸ mem_factoredNumbers_of_primeFactors_subset hm hp

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