isPrimePow_iff_minFac_pow_factorization_eq

English

IsPrimePow n iff n = minFac^v(minFac) where v(minFac) is the exponent from the prime factorization.

Русский

IsPrimePow n тогда и только тогда, когда n = minFac^{v(minFac)}.

LaTeX

$$$IsPrimePow(n)\iff n.minFac^{n.factorization(n.minFac)} = n$ (for n ≠ 1).$$

Lean4

theorem isPrimePow_iff_minFac_pow_factorization_eq {n : ℕ} (hn : n ≠ 1) :
    IsPrimePow n ↔ n.minFac ^ n.factorization n.minFac = n :=
  ⟨fun h => h.minFac_pow_factorization_eq, fun h => isPrimePow_of_minFac_pow_factorization_eq h hn⟩

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