p : ℕ
hp : Fact (Nat.Prime p)
a b : ℤ
ha : a ≠ 0
hb : b ≠ 0
⊢ padicValNat p (Int.natAbs (a * b)) = padicValNat p (Int.natAbs a) + padicValNat p (Int.natAbs b)
p : ℕ
hp : Fact (Nat.Prime p)
a b : ℤ
ha : a ≠ 0
hb : b ≠ 0
⊢ padicValInt p (a * b) = padicValInt p a + padicValInt p b
simp_rw [padicValInt]
no goals
p : ℕ
hp : Fact (Nat.Prime p)
a b : ℤ
ha : a ≠ 0
hb : b ≠ 0
⊢ padicValNat p (Int.natAbs (a * b)) = padicValNat p (Int.natAbs a) + padicValNat p (Int.natAbs b)
rw [Int.natAbs_mul, padicValNat.mul] <;> rwa [Int.natAbs_ne_zero]