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

State before:
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : ℕ
k : ℤ
hp : Nat.Prime p
h : SurjVal.v (primeVal hp) k = 0
⊢ decr_val_p p k = k
Tactic:
rw [decr_val_p]
State after:
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : ℕ
k : ℤ
hp : Nat.Prime p
h : SurjVal.v (primeVal hp) k = 0
⊢ (if (k % ↑p == 0) = true then k / ↑p else k) = k

State before:
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : ℕ
k : ℤ
hp : Nat.Prime p
h : SurjVal.v (primeVal hp) k = 0
⊢ (if (k % ↑p == 0) = true then k / ↑p else k) = k
Tactic:
aesop
State after:
no goals