Theorem: Int.nat_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 : ℕ
⊢ nat_valuation p (a * b) = nat_valuation p a + nat_valuation p b
Tactic:
convert nat_val_aux_mul_eq_add p prime prime.one_lt a b <;>
ext <;>
rw [(nat_valuation_of_one_lt p _ prime.one_lt)]
State after:
no goals