English
The p-adic valuation of a natural number n is the largest integer k such that p^k divides n, with the default value 0 when n = 0 or p = 1.
Русский
p-адическая оценка натурального числа n есть наибольшое целое k такое, что p^k делит n, и по умолчанию 0, если n = 0 или p = 1.
LaTeX
$$$\\\\mathrm{padicValNat}(p,n) = \\begin{cases}0, & (p = 1) \\lor (n = 0),\\\\[2pt] \\max\\\\{k \\\\in \\\\mathbb{N} : p^k \\\\mid n\\\\}, & \\text{иначе}.\\\\end{cases}$$$
Lean4
/-- For `p ≠ 1`, the `p`-adic valuation of a natural `n ≠ 0` is the largest natural number `k` such
that `p^k` divides `n`. If `n = 0` or `p = 1`, then `padicValNat p q` defaults to `0`. -/
def padicValNat (p : ℕ) (n : ℕ) : ℕ :=
if h : p ≠ 1 ∧ 0 < n then Nat.find (finiteMultiplicity_iff.2 h) else 0
