English
The cast of a+b in ZMod n equals the sum cast a + cast b with a possible subtraction of n depending on size.
Русский
Приведение суммы a+b в ZMod n равно привидению a+b в ZMod через вычитание n, если сумма превышает n.
LaTeX
$$$\\\\forall {n : \\\\mathbb{N}} (a b : ZMod n), \\\\operatorname{cast} (a + b) = \\\\operatorname{ite} (n \\\\le \\\\operatorname{cast} a + \\\\operatorname{cast} b) \\\\bigl( \\\\operatorname{cast} a + \\\\operatorname{cast} b - n \\\\bigr) \\\\bigl( \\\\operatorname{cast} a + \\\\operatorname{cast} b \\\\bigr)$$$$
Lean4
theorem cast_add_eq_ite {n : ℕ} (a b : ZMod n) :
(cast (a + b) : ℤ) = if (n : ℤ) ≤ cast a + cast b then (cast a + cast b - n : ℤ) else cast a + cast b :=
by
rcases n with - | n
· simp; rfl
change Fin (n + 1) at a b
change ((((a + b) : Fin (n + 1)) : ℕ) : ℤ) = if ((n + 1 : ℕ) : ℤ) ≤ (a : ℕ) + b then _ else _
simp only [Fin.val_add_eq_ite, Int.natCast_succ]
norm_cast
split_ifs with h
· rw [Nat.cast_sub h]
congr
· rfl
