Theorem: Int.primeVal_eq_zero_iff (ECTate/Algebra/ValuedRing.lean)

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