English
Let l and l' be lists over a type α. If their cyclic permutations are equal, then l = l'.
Русский
Пусть l и l' — списки над некоторым типом α. Если их циклические перестановки равны, то l = l'.
LaTeX
$$$$\forall l,l' : \mathrm{List}(\alpha), \operatorname{cyclicPermutations}(l) = \operatorname{cyclicPermutations}(l') \iff l = l'.$$$$
Lean4
@[simp]
theorem cyclicPermutations_inj {l l' : List α} : cyclicPermutations l = cyclicPermutations l' ↔ l = l' :=
cyclicPermutations_injective.eq_iff