English
Two lists are rotations of each other iff one can be obtained by rotating the other by some number of steps not exceeding the length of the first list.
Русский
Два списка являются вращениями друг друга тогда и только тогда, когда один можно получить поворотом другого на некоторое число шагов не превышающее длину первого списка.
LaTeX
$$$ l \sim_{\mathrm{rot}} l' \iff \exists n \le |l|, \; \text{rotate}(l,n) = l' $$$
Lean4
theorem isRotated_iff_mod : l ~r l' ↔ ∃ n ≤ l.length, l.rotate n = l' :=
by
refine ⟨fun h => ?_, fun ⟨n, _, h⟩ => ⟨n, h⟩⟩
obtain ⟨n, rfl⟩ := h
rcases l with - | ⟨hd, tl⟩
· simp
· refine ⟨n % (hd :: tl).length, ?_, rotate_mod _ _⟩
refine (Nat.mod_lt _ ?_).le
simp
