coe_int_add_eq_mod — Mathlib

English

For u,v in Fin(n), the integer value of u+v equals (u+v) mod n.

Русский

Для u,v ∈ Fin(n) целочисленное значение u+v равно (u+v) по модулю n.

LaTeX

$$$$((u+v:\mathrm{Fin}(n)):\mathbb{Z}) = ((u:\mathbb{Z})+(v:\mathbb{Z}))\bmod n.$$$$

Lean4

theorem coe_int_add_eq_mod {n : Nat} (u v : Fin n) : ((u + v : Fin n) : Int) = ((u : Int) + (v : Int)) % n := by
  omega
    -- Write `a + b` as `if (a + b : ℕ) < n then (a + b : ℤ) else (a + b : ℤ) - n` and
    -- similarly `a - b` as `if (b : ℕ) ≤ a then (a - b : ℤ) else (a - b : ℤ) + n`.

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