English
For any l and n, the element of l.rotate n at Fin index k (with appropriate modulus) equals the element of l at the corresponding index (k + n) mod length(l).
Русский
Для любого списка l и числа n элемент l.rotate n на позиции Fin k равен элементу l на соответствующей позиции (k + n) mod длина(l).
LaTeX
$$$\\forall {l:\\mathrm{List}\\alpha} (n:\\mathbb{N}) (k:\\mathbb{N}) \\rightarrow \\ l.rotate n .get \\langle k, _\\rangle = l.get \\langle (k + n) \\% |l|, _\\rangle$$$
Lean4
theorem rotate_eq_self_iff_eq_replicate [hα : Nonempty α] :
∀ {l : List α}, (∀ n, l.rotate n = l) ↔ ∃ a, l = replicate l.length a
| [] => by simp
| a :: l =>
⟨fun h =>
⟨a,
ext_getElem length_replicate.symm fun n h₁ h₂ => by
rw [getElem_replicate, ← Option.some_inj, ← getElem?_eq_getElem, ← head?_rotate h₁, h, head?_cons]⟩,
fun ⟨b, hb⟩ n => by rw [hb, rotate_replicate]⟩
