head_cyclicPermutations — Mathlib

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]

Похожие утверждения