intCast_val_sub_eq_sub_add_ite — Mathlib

English

For u,v in Fin(n), the integer cast of u−v satisfies the same piecewise relation as above: equals u−v with an added n when necessary.

Русский

Для u,v ∈ Fin(n) целочисленное отображение u−v следует той же разбиению по модулю: добавляем n при необходимости.

LaTeX

$$$$\text{See above: } (u-v)^{\mathbb{Z}} = u^{\mathbb{Z}}-v^{\mathbb{Z}}+ \begin{cases}0,& v\le u, \\ n,& \text{иначе} \end{cases}.$$$$

Lean4

theorem intCast_val_sub_eq_sub_add_ite {n : ℕ} (a b : Fin n) :
    ((a - b).val : ℤ) = a.val - b.val + if b ≤ a then 0 else n := by split <;> fin_omega

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