coe_int_add_eq_ite — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

theorem coe_int_add_eq_ite {n : Nat} (u v : Fin n) :
    ((u + v : Fin n) : Int) = if (u + v : ℕ) < n then (u + v : Int) else (u + v : Int) - n :=
  by
  rw [Fin.add_def]
  split
  · rw [natCast_emod, Int.emod_eq_of_lt] <;> omega
  · rw [natCast_emod, Int.emod_eq_sub_self_emod, Int.emod_eq_of_lt] <;> omega

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