primeFactors_subset_of_mem_smoothNumbers

English

The prime factors of a smooth number are contained in the primes below the bound.

Русский

Простые делители гладкого числа лежат среди простых ниже границы.

LaTeX

$$$m.\text{primeFactors} \subseteq n.\text{primesBelow}$, given $m \in n.\mathrm{smoothNumbers}$$$

Lean4

/-- The `Finset` of prime factors of an `n`-smooth number is contained in the `Finset`
of primes below `n`. -/
theorem primeFactors_subset_of_mem_smoothNumbers {m n : ℕ} (hms : m ∈ n.smoothNumbers) :
    m.primeFactors ⊆ n.primesBelow :=
  primeFactors_subset_of_mem_factoredNumbers <| smoothNumbers_eq_factoredNumbers_primesBelow n ▸ hms

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