rotate_perm — Mathlib

English

Rotation by n is a permutation of the list: l.rotate n ~ l.

Русский

Вращение на n является перестановкой списка: l.rotate n ~ l.

LaTeX

$$$\\forall \\alpha \\in \\mathsf{Type},\\forall l \\in \\mathsf{List}(\\alpha),\\ l.rotate n \\sim l$$$

Lean4

theorem rotate_perm (l : List α) (n : ℕ) : l.rotate n ~ l :=
  by
  rw [rotate_eq_rotate']
  induction n generalizing l with
  | zero => simp
  | succ n hn =>
    rcases l with - | ⟨hd, tl⟩
    · simp
    · rw [rotate'_cons_succ]
      exact (hn _).trans (perm_append_singleton _ _)

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