primeFactors_prime_pow

Mathlib.Data.Nat.PrimeFin

URI: https://scilib.ai/kg/mathlib#Nat.primeFactors_prime_pow

← MathLib Explorer

English

If p is prime and k > 0, then the prime factors of p^k are exactly {p}.

Русский

Если p простое и k > 0, то простые делители p^k равны {p}.

LaTeX

$$$ \\text{Prime}(p) \\Rightarrow (p^k).primeFactors = \\{ p \\}$$$

Lean4

/-- The only prime divisor of positive prime power `p^k` is `p` itself -/
theorem primeFactors_prime_pow (hk : k ≠ 0) (hp : Prime p) : (p ^ k).primeFactors = { p } := by
  simp [primeFactors_pow p hk, hp]

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

Научная платформа российской исследовательской школы.

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru