English
maxPowDiv(p, n) is a tail-recursive function that returns the largest k such that p^k divides n.
Русский
maxPowDiv(p, n) — хвостовая рекурсия, возвращающая наибольшее k, такое что p^k делит n.
LaTeX
$$$\\text{maxPowDiv}(p,n) = \\max\\{\,k \\in \\mathbb{N} : p^k \\mid n\\,\}$$$
Lean4
/-- Tail recursive function which returns the largest `k : ℕ` such that `p ^ k ∣ n` for any `p : ℕ`.
`padicValNat_eq_maxPowDiv` allows the code generator to use this definition for `padicValNat`
-/
def maxPowDiv (p n : ℕ) : ℕ :=
go 0 p n
where go (k p n : ℕ) : ℕ := if 1 < p ∧ 0 < n ∧ n % p = 0 then go (k + 1) p (n / p) else k
termination_by n
decreasing_by apply Nat.div_lt_self <;> tauto
