exact nat_val_mul_eq_add p prime (natAbs a) (natAbs b)
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)
no goals