formPerm_rotate — Mathlib

English

Rotating a nodup list by any number preserves the formPerm permutation.

Русский

Сдвиг любой величины у списка без повторов сохраняет перестановку formPerm.

LaTeX

$$$\forall \alpha\,[\DecidableEq\alpha] (l:\,\mathrm{List}\ \alpha),\mathrm{Nodup}\ l\rightarrow\forall n:\,\mathbb{N},\mathrm{formPerm}(l.rotate\ n)=\mathrm{formPerm}\ l$$$

Lean4

theorem formPerm_rotate (l : List α) (h : Nodup l) (n : ℕ) : formPerm (l.rotate n) = formPerm l := by
  induction n with
  | zero => simp
  | succ n hn =>
    rw [← rotate_rotate, formPerm_rotate_one, hn]
    rwa [IsRotated.nodup_iff]
    exact IsRotated.forall l n

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