val_add — Mathlib

English

For all n>0 and a,b ∈ ZMod n, the value of a+b equals the sum of values modulo n.

Русский

Для всех n>0 и a,b ∈ ZMod n, значение a+b равно сумме значений по модулю n.

LaTeX

$$$\forall n>0\forall a,b \in ZMod n,\ (a+b).\mathrm{val} = (a.\mathrm{val} + b.\mathrm{val}) \bmod n$$$

Lean4

theorem val_add {n : ℕ} [NeZero n] (a b : ZMod n) : (a + b).val = (a.val + b.val) % n :=
  by
  cases n
  · cases NeZero.ne 0 rfl
  · apply Fin.val_add

Похожие утверждения