finRotate — Mathlib

English

For every n, there is a permutation of Fin n that rotates elements one step to the right.

Русский

Для каждого n существует перестановка Fin n, которая сдвигает элементы на один шаг вправо.

LaTeX

$$$ \\forall n,\\; \\mathrm{Equiv.Perm}(\\mathrm{Fin}(n))$$$

Lean4

/-- Rotate `Fin n` one step to the right. -/
def finRotate : ∀ n, Equiv.Perm (Fin n)
  | 0 => Equiv.refl _
  | n + 1 => finAddFlip.trans (finCongr (Nat.add_comm 1 n))

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