padicValInt — Mathlib

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

Похожие утверждения