English
There is a natural bijection between the product of Nat with smoothNumbers p and smoothNumbers (p+1) given by (e, n) ↦ p^e · n when p is prime.
Русский
Существует естественная биекция между произведением ℕ × smoothNumbers(p) и smoothNumbers(p+1), заданная отображением (e, n) ↦ p^e · n при простоте p.
LaTeX
$$$\\mathrm{equivProdNatSmoothNumbers}(p, hp) : \\mathbb{N} \\times \\mathrm{smoothNumbers}(p) \\cong \\mathrm{smoothNumbers}(p+1)$$$
Lean4
/-- 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`. -/
theorem map_prime_pow_mul {F : Type*} [Mul F] {f : ℕ → F} (hmul : ∀ {m n}, Nat.Coprime m n → f (m * n) = f m * f n)
{p : ℕ} (hp : p.Prime) (e : ℕ) {m : p.smoothNumbers} : f (p ^ e * m) = f (p ^ e) * f m :=
hmul <| Coprime.pow_left _ <| hp.smoothNumbers_coprime <| Subtype.mem m
