English
For every n, the map l ↦ l.rotate n is injective; i.e., if l.rotate n = l'.rotate n, then l = l'.
Русский
Для каждого n отображение l ↦ l.rotate n инъективно; то есть если l.rotate n = l'.rotate n, то l = l'.
LaTeX
$$$\\forall n:\\mathbb{N}, \\mathrm{Injective} (\\lambda l: l.rotate n)$$$
Lean4
theorem rotate_injective (n : ℕ) : Function.Injective fun l : List α => l.rotate n :=
by
rintro l l' (h : l.rotate n = l'.rotate n)
have hle : l.length = l'.length := (l.length_rotate n).symm.trans (h.symm ▸ l'.length_rotate n)
rw [rotate_eq_drop_append_take_mod, rotate_eq_drop_append_take_mod] at h
obtain ⟨hd, ht⟩ := append_inj h (by simp_all)
rw [← take_append_drop _ l, ht, hd, take_append_drop]
