mem_smoothNumbers_iff_forall_le — Mathlib

English

The prime divisors of an n-smooth number are contained among the primes below n.

Русский

Простые делители n-гладкого числа принадлежат множеству простых ниже n.

LaTeX

$$$m \in n\text{.smoothNumbers} \Rightarrow m\text{.primeFactors} \subseteq n^{\text{primesBelow}}$$$

Lean4

/-- `m` is `n`-smooth if and only if `m` is nonzero and all prime divisors `≤ m` of `m`
are less than `n`. -/
theorem mem_smoothNumbers_iff_forall_le {n m : ℕ} : m ∈ smoothNumbers n ↔ m ≠ 0 ∧ ∀ p ≤ m, p.Prime → p ∣ m → p < n := by
  simp only [smoothNumbers_eq_factoredNumbers, mem_factoredNumbers_iff_forall_le, Finset.mem_range]

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