prodNatEquiv_symm_apply — Mathlib

English

The inverse map sends a prime power n to the pair (p,k) where p is the least prime factor and k = exponent of p in n minus 1.

Русский

Обратное отображение отправляет простую степень n в пару (p,k), где p — наименьший простой делитель, а k = показатель степени p в n минус 1.

LaTeX

$$$\text{prodNatEquiv}.\text{symm}(\langle n, \mathrm{IsPrimePow}(n)\rangle) = (\langle n.minFac, \mathrm{minFacPrime}(n.ne\_one)\rangle, n.factorization(n.minFac) - 1)$$$

Lean4

@[simp]
theorem prodNatEquiv_symm_apply {n : ℕ} (hn : IsPrimePow n) :
    prodNatEquiv.symm ⟨n, hn⟩ = (⟨n.minFac, minFac_prime hn.ne_one⟩, n.factorization n.minFac - 1) :=
  rfl

Похожие утверждения