English
There is a bijection between positive natural numbers and prime-supported exponent functions given by mapping n to its factorization and vice versa via a product over primes.
Русский
Существует биекция между положительными натуральными числами и функциями степеней над простыми, задаваемая факторизацией числа и обратной операцией через произведение по простым.
LaTeX
$$$\\mathrm{factorizationEquiv} : \\mathbb{N}_{+} \\simeq \\{f : \\mathbb{N} \\to \\mathbb{N} | \\forall p \\in \\mathrm{supp}(f), \\text{Prime}(p)\\}$$$
Lean4
/-- The equiv between `ℕ+` and `ℕ →₀ ℕ` with support in the primes. -/
def factorizationEquiv : ℕ+ ≃ {f : ℕ →₀ ℕ | ∀ p ∈ f.support, Prime p}
where
toFun := fun ⟨n, _⟩ => ⟨n.factorization, fun _ => prime_of_mem_primeFactors⟩
invFun := fun ⟨f, hf⟩ => ⟨f.prod _, prod_pow_pos_of_zero_notMem_support fun H => not_prime_zero (hf 0 H)⟩
left_inv := fun ⟨_, hx⟩ => Subtype.ext <| factorization_prod_pow_eq_self hx.ne.symm
right_inv := fun ⟨_, hf⟩ => Subtype.ext <| prod_pow_factorization_eq_self hf
