head?_cyclicPermutations

Mathlib.Data.List.Rotate

URI: https://scilib.ai/kg/mathlib#List.head?_cyclicPermutations

← MathLib Explorer

English

The head of the cyclicPermutations list equals the original list, as an option is Some l.

Русский

Голова списка cyclicPermutations равна исходному списку (в варианте Some l).

LaTeX

$$$ (\text{cyclicPermutations}~l).head? = \text{Some}~l $$$

Lean4

@[simp]
theorem head?_cyclicPermutations (l : List α) : (cyclicPermutations l).head? = l := by
  rw [head?_eq_head (cyclicPermutations_ne_nil l), head_cyclicPermutations]

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

Научная платформа российской исследовательской школы.

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru