English
Let p be a prime. For every x in Z_p and every n, there exists an integer a = appr(x,n) with 0 ≤ a < p^n such that x ≡ a (mod p^n).
Русский
Пусть p — простое число. Для каждого x ∈ ℤ_p и каждого n ∈ ℕ существует целое число a = appr(x,n) такое, что 0 ≤ a < p^n и x ≡ a (mod p^n).
LaTeX
$$$0 \le \operatorname{appr}(x,n) < p^n \quad\text{and}\quad x - \operatorname{appr}(x,n) \in (p^n)\mathbb{Z}_p$$$
Lean4
/-- `appr n x` gives a value `v : ℕ` such that `x` and `↑v : ℤ_p` are congruent mod `p^n`.
See `appr_spec`. -/
noncomputable def appr : ℤ_[p] → ℕ → ℕ
| _x, 0 => 0
| x, n + 1 =>
let y := x - appr x n
if hy : y = 0 then appr x n
else
let u := (unitCoeff hy : ℤ_[p])
appr x n + p ^ n * (toZMod ((u * (p : ℤ_[p]) ^ (y.valuation - n : ℤ).natAbs) : ℤ_[p])).val
