English
For any x and l with (x :: l) Nodup, and any n, (formPerm (x :: l)^n) x equals the element at position n modulo length.
Русский
Для любого x и l, если (x :: l) без повторов и для любого n, то (formPerm (x :: l))^n применяется к x даёт элемент на позиции n по модулю длины.
LaTeX
$$$\forall {\alpha:[DecidableEq\alpha]} (x:\,\alpha) (l:\,\mathrm{List}\ \alpha),\ (\mathrm{List}.Nodup\ (x :: l))\rightarrow\forall (n:\,\mathrm{Nat}),\ (\mathrm{formPerm}\ (x :: l)\ ^ n)\ x = (x :: l)[(n \\% (x :: l).length)]' (\\mathrm{Nat.mod\\_lt} _ (\\mathrm{Nat.zero\\_lt\\_succ} _))$$$
Lean4
theorem formPerm_pow_apply_getElem (l : List α) (w : Nodup l) (n : ℕ) (i : ℕ) (h : i < l.length) :
(formPerm l ^ n) l[i] = l[(i + n) % l.length]'(Nat.mod_lt _ (i.zero_le.trans_lt h)) := by
induction n with
| zero => simp [Nat.mod_eq_of_lt h]
| succ n hn => simp [pow_succ', mul_apply, hn, formPerm_apply_getElem _ w, ← Nat.add_assoc]
