primeFactors_pow

Mathlib.Data.Nat.PrimeFin

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

English

If k ≠ 0, then the prime factors of n^k equal the prime factors of n.

Русский

Если k ≠ 0, то простые делители n^k совпадают с простыми делителями n.

LaTeX

$$$ (k \\neq 0) \\Rightarrow (n^k).primeFactors = n.primeFactors $$$

Lean4

theorem primeFactors_pow (n : ℕ) (hk : k ≠ 0) : (n ^ k).primeFactors = n.primeFactors :=
  by
  cases k
  · simp at hk
  rw [primeFactors_pow_succ]

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

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

Разделы

Аффилиация

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