finRotate_succ_symm_apply — Mathlib

English

For i ∈ Fin n, the inverse of finRotate maps i to i − 1.

Русский

Обратное к finRotate на i даёт i − 1.

LaTeX

$$$ (\\mathrm{finRotate}(n))^{-1} i = i - 1 \\quad (i: \\mathrm{Fin}(n))$$$

Lean4

@[simp]
theorem finRotate_succ_symm_apply [NeZero n] (i : Fin n) : (finRotate _).symm i = i - 1 :=
  by
  obtain ⟨n, rfl⟩ := exists_eq_succ_of_ne_zero (NeZero.ne n)
  apply (finRotate n.succ).symm_apply_eq.mpr
  rw [finRotate_succ_apply, sub_add_cancel]

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