English
The cast is additive: (cast (a + b) : R) = cast a + cast b.
Русский
Приведение сохраняет сложение: cast(a+b) = cast a + cast b.
LaTeX
$$$\\\\forall {n : \\\\mathbb{N}} {R : Type*} [Ring R] {m : \\\\mathbb{N}} [CharP R m] (a b : ZMod n), \\\\operatorname{cast} (a + b) = \\\\operatorname{cast} a + \\\\operatorname{cast} b$$$
Lean4
@[simp]
theorem cast_mul (h : m ∣ n) (a b : ZMod n) : (cast (a * b : ZMod n) : R) = cast a * cast b :=
by
cases n
· apply Int.cast_mul
symm
dsimp [ZMod, ZMod.cast, ZMod.val]
rw [← Nat.cast_mul, Fin.val_mul, ← sub_eq_zero, ← Nat.cast_sub (Nat.mod_le _ _), @CharP.cast_eq_zero_iff R _ m]
exact h.trans (Nat.dvd_sub_mod _)
