English
Rotating a list then taking its cyclic permutations equals rotating the cyclic permutations of the list.
Русский
Поворот списка, затем взятие циклических перестановок, равно повороту циклических перестановок списка.
LaTeX
$$$$\forall l : \mathrm{List}(\alpha),\forall k : \mathbb{N}, (l.rotate\ k).cyclicPermutations = l.cyclicPermutations.rotate k.$$$$
Lean4
@[simp]
theorem cyclicPermutations_rotate (l : List α) (k : ℕ) :
(l.rotate k).cyclicPermutations = l.cyclicPermutations.rotate k :=
by
have : (l.rotate k).cyclicPermutations.length = length (l.cyclicPermutations.rotate k) :=
by
cases l
· simp
· rw [length_cyclicPermutations_of_ne_nil] <;> simp
refine ext_get this fun n hn hn' => ?_
rw [get_rotate, get_cyclicPermutations, rotate_rotate, ← rotate_mod, Nat.add_comm]
cases l <;> simp
