length_cyclicPermutations_cons

Mathlib.Data.List.Rotate

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

← MathLib Explorer

English

The length of cyclicPermutations (x :: l) equals length l plus 1.

Русский

Длина множества циклических перестановок списка (x :: l) равна длине l плюс 1.

LaTeX

$$$ \text{length}(\text{cyclicPermutations} (x :: l)) = \text{length}~l + 1 $$$

Lean4

theorem length_cyclicPermutations_cons (x : α) (l : List α) : length (cyclicPermutations (x :: l)) = length l + 1 := by
  simp [cyclicPermutations_cons]

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

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

Разделы

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

Аффилиация

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