val_add_eq_of_add_lt — Mathlib

English

For u,v in Fin(n), the integer value of u−v equals u−v plus n when v>u, otherwise u−v.

Русский

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

LaTeX

$$$$((u-v:\mathrm{Fin}(n)):\mathbb{Z}) = (u_{\mathrm{val}}-v_{\mathrm{val}}) + \begin{cases}0,& v\le u, \\ n,& \text{иначе} \end{cases}.$$$$

Lean4

theorem val_add_eq_of_add_lt {n : ℕ} {a b : Fin n} (huv : a.val + b.val < n) : (a + b).val = a.val + b.val :=
  by
  rw [val_add]
  simp [Nat.mod_eq_of_lt huv]

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