English
For all lists l and l', l ∈ cyclicPermutations(l') if and only if l is a rotation of l'.
Русский
Для любых списков l и l' верно: l принадлежит cyclicPermutations(l') тогда и только тогда, когда l является поворотом l'.
LaTeX
$$$$l \in \operatorname{cyclicPermutations}(l') \iff l \sim_r l'. $$$$
Lean4
@[simp]
theorem mem_cyclicPermutations_iff : l ∈ cyclicPermutations l' ↔ l ~r l' :=
by
constructor
· simp_rw [mem_iff_get, get_cyclicPermutations]
rintro ⟨k, rfl⟩
exact .forall _ _
· rintro ⟨k, rfl⟩
rw [cyclicPermutations_rotate, mem_rotate]
apply mem_cyclicPermutations_self