Smooth numbers #
We define the set
Nat.smoothNumbers n consisting of the positive natural numbers all of
whose prime factors are strictly less than
We also define the finite set
Nat.primesBelow n to be the set of prime numbers less than
f : ℕ → F is multiplicative on coprime arguments,
p is a prime and
f (p^e * m) = f (p^e) * f m.
- One or more equations did not get rendered due to their size.