English
For any lists l and l' and n, l.rotate n = l' if and only if l = l'.rotate (l'.length - n mod l'.length).
Русский
Для любых списков l и l' и n l.rotate n = l' тогда и только тогда, когда l = l'.rotate (l'.length - n mod l'.length).
LaTeX
$$$\\forall {l\\, l' : \\mathrm{List}\\alpha} {n : \\mathbb{N}}, \\ l.rotate n = l' \\iff \\ l = l'.rotate (l'.length - n \\% l'.length)$$$
Lean4
theorem rotate_eq_iff {l l' : List α} {n : ℕ} : l.rotate n = l' ↔ l = l'.rotate (l'.length - n % l'.length) :=
by
rw [← @rotate_eq_rotate _ l _ n, rotate_rotate, ← rotate_mod l', add_mod]
rcases l'.length.zero_le.eq_or_lt with hl | hl
· rw [eq_nil_of_length_eq_zero hl.symm, rotate_nil]
· rcases (Nat.zero_le (n % l'.length)).eq_or_lt with hn | hn
· simp [← hn]
· rw [mod_eq_of_lt (Nat.sub_lt hl hn), Nat.sub_add_cancel, mod_self, rotate_zero]
exact (Nat.mod_lt _ hl).le
