Commit 2023-11-11 15:52 1cb42bfd

feat: add definition of and statements about the set of smooth numbers (#8252) 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. This is in preparation of Euler Products; see this Zulip thread.