n : ℤ
k p : ℕ
hp : Nat.Prime p
h : p ∣ natAbs n ^ k
⊢ p ∣ natAbs n
n : ℤ
k p : ℕ
hp : Nat.Prime p
h : ↑p ∣ n ^ k
⊢ p ∣ natAbs n
rw [Int.coe_nat_dvd_left, Int.natAbs_pow] at h
no goals
n : ℤ
k p : ℕ
hp : Nat.Prime p
h : p ∣ natAbs n ^ k
⊢ p ∣ natAbs n
exact hp.dvd_of_dvd_pow h