Smooth numbers #

We define the set Nat.smoothNumbers n consisting of the positive natural numbers all of whose prime factors are strictly less than n.

We also define the finite set Nat.primesBelow n to be the set of prime numbers less than n.

The main definition Nat.equivProdNatSmoothNumbers establishes the bijection between ℕ × (smoothNumbers p) and smoothNumbers (p+1) given by sending (e, n) to p^e * n. Here p is a prime number.

primesBelow n is the set of primes less than n as a finset.

Instances For
    theorem Nat.lt_of_mem_primesBelow {p : } {n : } (h : p Nat.primesBelow n) :
    p < n

    smoothNumbers n is the set of n-smooth positive natural numbers, i.e., the positive natural numbers all of whose prime factors are less than n.

    Instances For
      theorem Nat.mem_smoothNumbers {n : } {m : } :
      m Nat.smoothNumbers n m 0 pNat.factors m, p < n
      theorem Nat.mem_smoothNumbers' {n : } {m : } :
      m Nat.smoothNumbers n ∀ (p : ), Nat.Prime pp mp < n

      m is n-smooth if and only if all prime divisors of m are less than n.

      The product of the prime factors of n that are less than N is an N-smooth number.

      The sets of N-smooth and of (N+1)-smooth numbers are the same when N is not prime. See Nat.equivProdNatSmoothNumbers for when N is prime.

      theorem Nat.smoothNumbers_compl (N : ) :
      (Nat.smoothNumbers N) \ {0} {n : | N n}

      The non-zero non-N-smooth numbers are ≥ N.

      theorem Nat.pow_mul_mem_smoothNumbers {p : } {n : } (hp : p 0) (e : ) (hn : n Nat.smoothNumbers p) :

      If p is positive and n is p-smooth, then every product p^e * n is (p+1)-smooth.

      If p is a prime and n is p-smooth, then p and n are coprime.

      theorem Nat.map_prime_pow_mul {F : Type u_1} [CommSemiring F] {f : F} (hmul : ∀ {m n : }, Nat.Coprime m nf (m * n) = f m * f n) {p : } (hp : Nat.Prime p) (e : ) {m : (Nat.smoothNumbers p)} :
      f (p ^ e * m) = f (p ^ e) * f m

      If f : ℕ → F is multiplicative on coprime arguments, p is a prime and m is p-smooth, then f (p^e * m) = f (p^e) * f m.

      We establish the bijection from ℕ × smoothNumbers p to smoothNumbers (p+1) given by (e, n) ↦ p^e * n when p is a prime. See Nat.smoothNumbers_succ for when p is not prime.

      • One or more equations did not get rendered due to their size.
      Instances For
        theorem Nat.equivProdNatSmoothNumbers_apply {p : } {e : } {m : } (hp : Nat.Prime p) (hm : m Nat.smoothNumbers p) :
        ((Nat.equivProdNatSmoothNumbers hp) (e, { val := m, property := hm })) = p ^ e * m
        theorem Nat.equivProdNatSmoothNumbers_apply' {p : } (hp : Nat.Prime p) (x : × (Nat.smoothNumbers p)) :
        ((Nat.equivProdNatSmoothNumbers hp) x) = p ^ x.1 * x.2