English
The natural-valued map val sends an element of ZMod n to a canonical representative: for n = 0 it is the natAbs of the integer, for n > 0 it is the natural representative of its class.
Русский
Функция val выбирает естественно-числового представителя класса: для n = 0 это natAbs, для n > 0 — естественный представитель Fin(n).
LaTeX
$$$ \text{def } \mathrm{val}: \forall \{n : \mathbb{N}\}, \mathrm{ZMod}\ n \to \mathbb{N} \;|\; 0 \mapsto \mathrm{Int}.\mathrm{natAbs} \;|\; n+1 \mapsto (\uparrow:\mathrm{Fin}(n+1) \to \mathbb{N})$$$
Lean4
/-- `val a` is a natural number defined as:
- for `a : ZMod 0` it is the absolute value of `a`
- for `a : ZMod n` with `0 < n` it is the least natural number in the equivalence class
See `ZMod.valMinAbs` for a variant that takes values in the integers.
-/
def val : ∀ {n : ℕ}, ZMod n → ℕ
| 0 => Int.natAbs
| n + 1 => ((↑) : Fin (n + 1) → ℕ)
