factorization_pow — Mathlib

English

If p is prime, then (p^k).factorization = single p k.

Русский

Если p простое, то факторизация p^k равна единственному простому фактору p с показателем k.

LaTeX

$$$\\text{Prime}(p) \\Rightarrow (p^k).factorization = \\mathrm{single}\\ p\\ k$$$

Lean4

/-- For prime `p` the only prime factor of `p^k` is `p` with multiplicity `k` -/
theorem factorization_pow {p k : ℕ} (hp : Prime p) : (p ^ k).factorization = single p k := by simp [hp]

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