rw [primeVal, int_valuation_eq_zero_iff hp.one_lt, Int.dvd_iff_emod_eq_zero]
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : ℕ
k : ℤ
hp : Nat.Prime p
⊢ SurjVal.v (primeVal hp) k = 0 ↔ ¬↑p ∣ k
no goals