English
The p-adic valuation of an integer z is the p-adic valuation of its absolute value as a natural number: padicValInt(p,z) = padicValNat(p, |z|).
Русский
p‑адическая оценка целого z равна p‑адикальной оценке его абсолютного значения: padicValInt(p,z) = padicValNat(p, |z|).
LaTeX
$$$\mathrm{padicValInt}(p,z) = \mathrm{padicValNat}(p,|z|)$$$
Lean4
/-- For `p ≠ 1`, the `p`-adic valuation of an integer `z ≠ 0` is the largest natural number `k` such
that `p^k` divides `z`. If `x = 0` or `p = 1`, then `padicValInt p q` defaults to `0`. -/
def padicValInt (p : ℕ) (z : ℤ) : ℕ :=
padicValNat p z.natAbs