formPerm_eq_of_isRotated — Mathlib

English

For any list l and elements a,b, formPerm (l ++ [a,b]) equals formPerm (l ++ [a]) multiplied by swap a b.

Русский

Для любого списка l и элементов a,b имеет место formPerm (l ++ [a,b]) = formPerm (l ++ [a]) · swap a b.

LaTeX

$$$\forall {\alpha}:{\rm Type},\,[{\rm DecidableEq}\ \alpha]\ forall (l:\,\mathrm{List}\ \alpha) (a b:\,\alpha),\ \mathrm{formPerm}(l++[a,b])=\mathrm{formPerm}(l++[a])\ast \mathrm{swap}\ a\ b$$$

Lean4

theorem formPerm_eq_of_isRotated {l l' : List α} (hd : Nodup l) (h : l ~r l') : formPerm l = formPerm l' :=
  by
  obtain ⟨n, rfl⟩ := h
  exact (formPerm_rotate l hd n).symm

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