English
For any l, n, k with k < length(l), the element at position k in l.rotate n equals the element of l at position (length(l) - (n mod length(l)) + k) mod length(l).
Русский
Для любого списка l и любого n, и любого k < length(l), элемент на позиции k в l.rotate n равен элементу l на позиции (length(l) - (n mod length(l)) + k) mod length(l).
LaTeX
$$$\\forall l\\in\\mathrm{List}\\alpha,\\forall n\\in\\mathbb{N},\\forall k\\in\\mathbb{N},\\hk:\\ k < |l| \\Rightarrow l[k] = (l.rotate n)[( |l| - (n \\% |l|) + k) \\% |l|]$$$
Lean4
theorem getElem_rotate (l : List α) (n : ℕ) (k : Nat) (h : k < (l.rotate n).length) :
(l.rotate n)[k] = l[(k + n) % l.length]'(mod_lt _ (length_rotate l n ▸ k.zero_le.trans_lt h)) :=
by
rw [← Option.some_inj, ← getElem?_eq_getElem, ← getElem?_eq_getElem, getElem?_rotate]
exact h.trans_eq (length_rotate _ _)
