English
Rotating a list by one position does not change its associated formPerm permutation.
Русский
Сдвиг списка на одну позицию не изменяет соответствующую перестановку formPerm.
LaTeX
$$$\forall \alpha\,[\DecidableEq\alpha]\forall l:\,\mathrm{List}\ \alpha,\mathrm{Nodup}\ l\rightarrow\mathrm{formPerm}(l.rotate\ 1)=\mathrm{formPerm}\ l$$$
Lean4
theorem formPerm_rotate_one (l : List α) (h : Nodup l) : formPerm (l.rotate 1) = formPerm l :=
by
have h' : Nodup (l.rotate 1) := by simpa using h
ext x
by_cases hx : x ∈ l.rotate 1
· obtain ⟨k, hk, rfl⟩ := getElem_of_mem hx
rw [formPerm_apply_getElem _ h', getElem_rotate l, getElem_rotate l, formPerm_apply_getElem _ h]
simp
· rw [formPerm_apply_of_notMem hx, formPerm_apply_of_notMem]
simpa using hx
