English
Let p be a prime and x an element of the p-adic integers ℤ_p. Then there exists a unique integer y with 0 ≤ y < p such that x − y lies in the unique maximal ideal of ℤ_p; this y is the residue of x modulo p, i.e., zmodRepr(x) = y.
Русский
Пусть p — простое число и x ∈ ℤ_p. Существует единственное целое y с 0 ≤ y < p, такое что x − y ∈ maximalIdeal(ℤ_p). Это y является остатком x по модулю p, то есть zmodRepr(x) = y.
LaTeX
$$$\forall x \in \mathbb{Z}_{(p)}\;\exists! y \in \{0,1,\dots,p-1\},\; x - y \in \mathfrak{m}_{\mathbb{Z}_{(p)}}$,$$
Lean4
/-- `zmodRepr x` is the unique natural number smaller than `p`
satisfying `‖(x - zmodRepr x : ℤ_[p])‖ < 1`.
-/
def zmodRepr : ℕ :=
Classical.choose (existsUnique_mem_range x).exists
