finRotate_succ_apply — Mathlib

English

For all i : Fin(n+1), finRotate(n+1) i = i + 1.

Русский

Для всех i ∈ Fin(n+1), finRotate(n+1) i = i + 1.

LaTeX

$$$ \\forall i : \\mathrm{Fin}(n+1),\\; \\mathrm{finRotate}(n+1)\\,i = i + 1$$$

Lean4

@[simp]
theorem finRotate_succ_apply (i : Fin (n + 1)) : finRotate (n + 1) i = i + 1 :=
  by
  cases n
  · exact @Subsingleton.elim (Fin 1) _ _ _
  obtain rfl | h := Fin.eq_or_lt_of_le i.le_last
  · simp [finRotate_last]
  · cases i
    simp only [Fin.lt_iff_val_lt_val, Fin.val_last] at h
    simp [finRotate_of_lt h, Fin.add_def, Nat.mod_eq_of_lt (Nat.succ_lt_succ h)]

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