val_add_eq_ite — Mathlib

English

For u,v in Fin(n), the numeric value of u+v is u+v if u+v < n, else u+v−n.

Русский

Для u,v ∈ Fin(n) числовое значение u+v равно u+v, если u+v < n, иначе u+v−n.

LaTeX

$$$$((u+v:\mathrm{Fin}(n)):\mathbb{N}) = \begin{cases} u+v, & (u+v) < n \\ u+v-n, & \text{иначе} \end{cases}.$$$$

Lean4

theorem val_add_eq_ite {n : ℕ} (a b : Fin n) : (↑(a + b) : ℕ) = if n ≤ a + b then a + b - n else a + b := by
  rw [Fin.val_add, Nat.add_mod_eq_ite, Nat.mod_eq_of_lt (show ↑a < n from a.2), Nat.mod_eq_of_lt (show ↑b < n from b.2)]

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