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

State before:
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : ℕ
prime : Nat.Prime p
a b : ℤ
⊢ int_val p (a * b) = int_val p a + int_val p b
Tactic:
simp [int_val, natAbs_mul]
State after:
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : ℕ
prime : Nat.Prime p
a b : ℤ
⊢ nat_valuation p (natAbs a * natAbs b) = nat_valuation p (natAbs a) + nat_valuation p (natAbs b)

State before:
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : ℕ
prime : Nat.Prime p
a b : ℤ
⊢ nat_valuation p (natAbs a * natAbs b) = nat_valuation p (natAbs a) + nat_valuation p (natAbs b)
Tactic:
exact nat_val_mul_eq_add p prime (natAbs a) (natAbs b)
State after:
no goals