English
For any a ∈ Int, for NeZero n, ↑(a : ZMod n).val = a % n in the appropriate ring.
Русский
Для любого a ∈ ℤ и не нуля n, оболочка (a : ZMod n).val даёт a mod n.
LaTeX
$$$ \uparrow (a : ZMod n).\mathrm{val} = a \bmod n $$$
Lean4
theorem val_intCast {n : ℕ} (a : ℤ) [NeZero n] : ↑(a : ZMod n).val = a % n :=
by
have hle : (0 : ℤ) ≤ ↑(a : ZMod n).val := Int.natCast_nonneg _
have hlt : ↑(a : ZMod n).val < (n : ℤ) := Int.ofNat_lt.mpr (ZMod.val_lt a)
refine (Int.emod_eq_of_lt hle hlt).symm.trans ?_
rw [← ZMod.intCast_eq_intCast_iff', Int.cast_natCast, ZMod.natCast_val, ZMod.cast_id]