English
For any list l and k with k in the range of l.rotate 1, the k-th element of l.rotate 1 equals the element of l at index (k + 1) mod length(l).
Русский
Для любого списка l и k, принадлежащего диапазону l.rotate 1, k-й элемент l.rotate 1 равен элементу l на индексе (k + 1) mod длины(l).
LaTeX
$$$\\forall {l\\in\\mathrm{List}\\alpha} (k:\\mathrm{Fin}(|l.rotate 1|)), \\ (l.rotate 1).get k = l.get \\langle (k.1 + 1) \\% |l|, \\rangle$$$
Lean4
theorem rotate_one_eq_self_iff_eq_replicate [Nonempty α] {l : List α} :
l.rotate 1 = l ↔ ∃ a : α, l = List.replicate l.length a :=
⟨fun h =>
rotate_eq_self_iff_eq_replicate.mp fun n =>
Nat.rec l.rotate_zero (fun n hn => by rwa [Nat.succ_eq_add_one, ← l.rotate_rotate, hn]) n,
fun h => rotate_eq_self_iff_eq_replicate.mpr h 1⟩
