English
The head of the cyclicPermutations list is the original list.
Русский
Голова списка cyclicPermutations равна исходному списку.
LaTeX
$$$ (\text{cyclicPermutations}~l).head~(\text{cyclicPermutations\_ne\_nil}~l) = l $$$
Lean4
@[simp]
theorem head_cyclicPermutations (l : List α) : (cyclicPermutations l).head (cyclicPermutations_ne_nil l) = l :=
by
have h : 0 < length (cyclicPermutations l) := length_pos_of_ne_nil (cyclicPermutations_ne_nil _)
rw [← get_mk_zero h, get_cyclicPermutations, Fin.val_mk, rotate_zero]