English
There is a specific equivalence between ℕ × smoothNumbers p and smoothNumbers (p+1) when p is prime, realized by a composition of natural-congruences and factoredNumbers.
Русский
Существует конкретное соответствие между ℕ × smoothNumbers(p) и smoothNumbers(p+1) при простоте p, реализуемое через композицию отображений и факторизаций.
LaTeX
$$$\mathrm{equivProdNatSmoothNumbers} : \mathbb{N} \times \mathrm{smoothNumbers}(p) \simeq \mathrm{smoothNumbers}(p+1)$$$
Lean4
/-- 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. -/
def equivProdNatSmoothNumbers {p : ℕ} (hp : p.Prime) : ℕ × smoothNumbers p ≃ smoothNumbers (p + 1) :=
((prodCongrRight fun _ ↦ setCongr <| smoothNumbers_eq_factoredNumbers p).trans <|
equivProdNatFactoredNumbers hp Finset.notMem_range_self).trans <|
setCongr <| (smoothNumbers_eq_factoredNumbers (p + 1)) ▸ Finset.range_add_one ▸ rfl
