primeFactors_pow_succ — Mathlib

English

For all n,k, the prime factors of n^(k+1) are exactly the prime factors of n.

Русский

Для любых n и k простые делители n^(k+1) совпадают с простыми делителями n.

LaTeX

$$$ (n^{k+1}).primeFactors = n.primeFactors $$$

Lean4

theorem primeFactors_pow_succ (n k : ℕ) : (n ^ (k + 1)).primeFactors = n.primeFactors :=
  by
  rcases eq_or_ne n 0 with (rfl | hn)
  · simp
  induction k with
  | zero => simp
  | succ k ih => rw [pow_succ', primeFactors_mul hn (pow_ne_zero _ hn), ih, Finset.union_idempotent]

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