English
If a list l has no duplicates, then its cyclic permutations are all distinct.
Русский
Если у списка l нет повторяющихся элементов, то все его циклические перестановки различны.
LaTeX
$$$$\operatorname{Nodup}(l) \Rightarrow \operatorname{Nodup}(\operatorname{cyclicPermutations}(l)).$$$$
Lean4
/-- If a `l : List α` is `Nodup l`, then all of its cyclic permutants are distinct. -/
protected theorem cyclicPermutations {l : List α} (hn : Nodup l) : Nodup (cyclicPermutations l) :=
by
rcases eq_or_ne l [] with rfl | hl
· simp
· rw [nodup_iff_injective_get]
rintro ⟨i, hi⟩ ⟨j, hj⟩ h
simp only [length_cyclicPermutations_of_ne_nil l hl] at hi hj
simpa [hn.rotate_congr_iff, mod_eq_of_lt, *] using h
