cyclicPermutations_ne_nil

Mathlib.Data.List.Rotate

URI: https://scilib.ai/kg/mathlib#List.cyclicPermutations_ne_nil

English

For any α-list l, l.cyclicPermutations is nonempty.

Русский

Для любого списка l на языке α множество cyclicPermutations(l) не пусто.

LaTeX

$$$ \forall l:\text{List}(\alpha), \; l.cyclicPermutations \neq [] $$$

Lean4

@[simp]
theorem cyclicPermutations_ne_nil : ∀ l : List α, cyclicPermutations l ≠ []
  | a :: l, h => by simpa using congr_arg length h

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

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

Разделы

Аффилиация

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