English
For Nodup l, for i and h that i < length l, (formPerm l)^n applied to the nth element yields the (i+n)th element modulo length, with the appropriate mod.
Русский
Для Nodup l, для i и h, что i < length l, (formPerm l)^n действует на i-й элемент так, что получаем элемент (i+n) по модулю длины.
LaTeX
$$$\forall {\alpha:\,Type},\[\DecidableEq\alpha],\ (l:\,\mathrm{List}\ \alpha),\ l.Nodup\rightarrow\forall (n:\,\mathrm{Nat}) (i:\,\mathrm{Nat}) (h:\, i < l.length),\ (formPerm\ l\^ n)\ l[i] = l[(i+n) \% l.length]'(\\mathrm{Nat.mod\\_lt} _ (i.0).trans(h))$$$
Lean4
theorem formPerm_pow_apply_head (x : α) (l : List α) (h : Nodup (x :: l)) (n : ℕ) :
(formPerm (x :: l) ^ n) x = (x :: l)[(n % (x :: l).length)]'(Nat.mod_lt _ (Nat.zero_lt_succ _)) :=
by
convert formPerm_pow_apply_getElem _ h n 0 (Nat.succ_pos _)
simp
