primeFactorsList_pow — Mathlib

English

For a prime p and any n, the prime factors list of p^n consists of n copies of p.

Русский

Для простого p и любого n список простых делителей p^n состоит из n копий p.

LaTeX

$$p \text{ Prime} \rightarrow \forall n, (p^n).primeFactorsList = List.replicate(n, p)$$

Lean4

theorem primeFactorsList_pow {p : ℕ} (hp : p.Prime) (n : ℕ) : (p ^ n).primeFactorsList = List.replicate n p :=
  by
  symm
  rw [← List.replicate_perm]
  apply Nat.primeFactorsList_unique (List.prod_replicate n p)
  intro q hq
  rwa [eq_of_mem_replicate hq]

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