factors_prime_pow — Mathlib

English

If p is irreducible, then the factors of p^k are exactly k copies of p (as an associated class).

Русский

Если p неприводимо, то разложение p^k состоит ровно из k копий p (как ассоциированных).

LaTeX

$$$$\\forall p\\,hp\\,\\forall k:\\; \\mathrm{factors}(p^k) = \\mathrm{WithTop}.\\mathrm{some}\\, \\mathrm{Multiset}.\\mathrm{replicate}(k, \\langle p,hp\\rangle).$$$$

Lean4

theorem factors_prime_pow [Nontrivial α] {p : Associates α} (hp : Irreducible p) (k : ℕ) :
    factors (p ^ k) = WithTop.some (Multiset.replicate k ⟨p, hp⟩) :=
  FactorSet.unique
    (by
      rw [Associates.factors_prod, FactorSet.prod.eq_def]
      dsimp; rw [Multiset.map_replicate, Multiset.prod_replicate, Subtype.coe_mk])

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