# Documentation

Mathlib.NumberTheory.SmoothNumbers

# 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.

def Nat.primesBelow (n : ) :

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

Equations
Instances For
@[simp]
theorem Nat.prime_of_mem_primesBelow {p : } {n : } (h : ) :
theorem Nat.lt_of_mem_primesBelow {p : } {n : } (h : ) :
p < n
theorem Nat.primesBelow_succ (n : ) :
= if then else
theorem Nat.not_mem_primesBelow (n : ) :
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.

Equations
Instances For
theorem Nat.mem_smoothNumbers {n : } {m : } :
m 0 p, p < n
theorem Nat.mem_smoothNumbers' {n : } {m : } :
∀ (p : ), p mp < n

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

@[simp]
theorem Nat.prod_mem_smoothNumbers (n : ) (N : ) :
List.prod (List.filter (fun (x : ) => decide (x < N)) ())

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

theorem Nat.smoothNumbers_succ {N : } (hN : ) :

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.

@[simp]
theorem Nat.smoothNumbers_one :
= {1}
theorem Nat.smoothNumbers_mono {N : } {M : } (hNM : N M) :
theorem Nat.smoothNumbers_compl (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 : ) :
p ^ e * n

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

theorem Nat.Prime.smoothNumbers_coprime {p : } {n : } (hp : ) (hn : ) :

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} [] {f : F} (hmul : ∀ {m n : }, f (m * n) = f m * f n) {p : } (hp : ) (e : ) {m : } :
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.

def Nat.equivProdNatSmoothNumbers {p : } (hp : ) :
× ()

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.

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