Theorems · Theorem · number theory

Nat.roughNumbersUpTo_eq_biUnion

∀ (N k : ℕ),
  N.roughNumbersUpTo k =
    ((N + 1).primesBelow \ k.primesBelow).biUnion fun p => {m ∈ Finset.range (N + 1) | m ≠ 0 ∧ p ∣ m}

The set of k-rough numbers ≤ N can be written as the union of the sets of multiples ≤ N of primes k ≤ p ≤ N.

Defined in

Mathlib.NumberTheory.SmoothNumbers

Cited by

1 results in Mathlib

Foundations

Depth 87 from the axioms · uses propext, Classical.choice, Quot.sound