isPrimePow_of_has_chain — Mathlib

English

If q is a prime power in a UniqueFactorizationMonoid, then q is a prime power.

Русский

Если q является простой степенью в факторизующем моноиде, то q — простая степень.

LaTeX

$$$\mathrm{IsPrimePow}(q)$$$

Lean4

theorem isPrimePow_of_has_chain {q : Associates M} {n : ℕ} (hn : n ≠ 0) {c : Fin (n + 1) → Associates M}
    (h₁ : StrictMono c) (h₂ : ∀ {r : Associates M}, r ≤ q ↔ ∃ i, r = c i) (hq : q ≠ 0) : IsPrimePow q :=
  ⟨c 1, n, irreducible_iff_prime.mp (second_of_chain_is_irreducible hn h₁ (@h₂) hq), zero_lt_iff.mpr hn,
    (eq_pow_second_of_chain_of_has_chain hn h₁ (@h₂) hq).symm⟩

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