p : ℕ
hp : Prime p
n : ℕ
⊢ replicate n p = factors (p ^ n)
p : ℕ
hp : Prime p
n : ℕ
⊢ factors (p ^ n) = replicate n p
symm
p : ℕ
hp : Prime p
n : ℕ
⊢ replicate n p ~ factors (p ^ n)
p : ℕ
hp : Prime p
n : ℕ
⊢ replicate n p = factors (p ^ n)
rw [← List.replicate_perm]
p : ℕ
hp : Prime p
n : ℕ
⊢ ∀ (p_1 : ℕ), p_1 ∈ replicate n p → Prime p_1
p : ℕ
hp : Prime p
n : ℕ
⊢ replicate n p ~ factors (p ^ n)
apply Nat.factors_unique (List.prod_replicate n p)
p : ℕ
hp : Prime p
n q : ℕ
hq : q ∈ replicate n p
⊢ Prime q
p : ℕ
hp : Prime p
n : ℕ
⊢ ∀ (p_1 : ℕ), p_1 ∈ replicate n p → Prime p_1
intro q hq
no goals
p : ℕ
hp : Prime p
n q : ℕ
hq : q ∈ replicate n p
⊢ Prime q
rwa [eq_of_mem_replicate hq]