coe_int_sub_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_sub_eq_mod {n : Nat} (u v : Fin n) : ((u - v : Fin n) : Int) = ((u : Int) - (v : Int)) % n :=
  by
  rw [coe_int_sub_eq_ite]
  split
  · rw [Int.emod_eq_of_lt] <;> omega
  · rw [Int.emod_eq_add_self_emod, Int.emod_eq_of_lt] <;> omega

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