English
There is a canonical bijection between pairs (p,k) with p prime and k ∈ ℕ and the set of prime powers, given by (p,k) ↦ p^(k+1). The inverse sends n (a prime power) to (minFac(n), exponent(n)−1).
Русский
Существует каноническая биекция между парами (p,k) с p простым и k ∈ ℕ и множеством степеней простого: (p,k) ↦ p^(k+1); обратное сопоставление отправляет n, являющееся степенью простого, в пару (minFac(n), exponent(n)−1).
LaTeX
$$$\text{There is a natural bijection }(p,k) \leftrightarrow n\text{ with } \text{IsPrimePow}(n)\text{ given by }(p,k) \mapsto p^{k+1}\text{ and }n \mapsto (\langle n.minFac, \text{minFacPrime}(n.prop) \rangle, n.factorization(n.minFac) - 1).$$$
Lean4
/-- The canonical equivalence between pairs `(p, k)` with `p` a prime and `k : ℕ`
and the set of prime powers given by `(p, k) ↦ p^(k+1)`. -/
def prodNatEquiv : Nat.Primes × ℕ ≃ { n : ℕ // IsPrimePow n }
where
toFun pk := ⟨pk.1 ^ (pk.2 + 1), ⟨pk.1, pk.2 + 1, prime_iff.mp pk.1.prop, pk.2.add_one_pos, rfl⟩⟩
invFun n := (⟨n.val.minFac, minFac_prime n.prop.ne_one⟩, n.val.factorization n.val.minFac - 1)
left_inv := fun (p, k) ↦ by
simp only [p.prop.pow_minFac k.add_one_ne_zero, Subtype.coe_eta, factorization_pow, p.prop, Prime.factorization,
Finsupp.smul_single, smul_eq_mul, mul_one, Finsupp.single_add, Finsupp.coe_add, Pi.add_apply,
Finsupp.single_eq_same, add_tsub_cancel_right]
right_inv
n := by
ext1
dsimp only
rw [sub_one_add_one (Nat.factorization_minFac_ne_zero n.prop.one_lt), n.prop.minFac_pow_factorization_eq]
