English
For each n, valMinAbs assigns to every element of ZMod n the integer in the same residue class that lies closest to zero, lying in the interval (-n/2, n/2].
Русский
Для каждого n функция valMinAbs присваивает каждому элементу ZMod n целое число из той же клаccа остатка, ближайшее к нулю, принадлежащее интервалу (-n/2, n/2].
LaTeX
$$$$ \\mathrm{valMinAbs} : \\forall n, \\mathbb{Z}/n\\mathbb{Z} \\to \\mathbb{Z}, \\text{ sending each class to the closest representative} $$$$
Lean4
/-- Returns the integer in the same equivalence class as `x` that is closest to `0`.
The result will be in the interval `(-n/2, n/2]`. -/
def valMinAbs : ∀ {n : ℕ}, ZMod n → ℤ
| 0, x => x
| n@(_ + 1), x => if x.val ≤ n / 2 then x.val else (x.val : ℤ) - n
