coe_finRotate — Mathlib

English

The coe of finRotate(n+1) is piecewise: it is 0 when i is the last element, otherwise i+1.

Русский

Образ по числу от finRotate(n+1) задаётся по кускам: 0 если i — последний элемент, иначе i+1.

LaTeX

$$$ (\\mathrm{finRotate}(n+1) i) = \\begin{cases} 0, & i = \\mathrm{Fin.last}(n) \\\\ i+1, & \\text{otherwise} \\end{cases} $$$

Lean4

theorem coe_finRotate (i : Fin n.succ) : (finRotate n.succ i : ℕ) = if i = Fin.last n then (0 : ℕ) else i + 1 := by
  rw [finRotate_succ_apply, Fin.val_add_one i]

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