English
For any n > 0 and a ∈ ZMod n, the value of the negation is 0 if a = 0, and n − a.val otherwise; equivalently, (-a).val = ind(a ≠ 0)·(n − a.val).
Русский
Для любого n > 0 и a ∈ ZMod n, значение отрицания равно 0, если a = 0, иначе n − a.val; то есть (-a).val = 0 если a = 0 иначе = n − a.val.
LaTeX
$$$(-a).val = \begin{cases}0, & \text{if } a = 0 \\ n - a.val, & \text{otherwise} \end{cases}$$$
Lean4
theorem neg_val {n : ℕ} [NeZero n] (a : ZMod n) : (-a).val = if a = 0 then 0 else n - a.val :=
by
rw [neg_val']
by_cases h : a = 0; · rw [if_pos h, h, val_zero, tsub_zero, Nat.mod_self]
rw [if_neg h]
apply Nat.mod_eq_of_lt
apply Nat.sub_lt (NeZero.pos n)
contrapose! h
rwa [Nat.le_zero, val_eq_zero] at h
