get_cyclicPermutations

Mathlib.Data.List.Rotate

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

English

For any l, n with n in Fin(length(cyclicPermutations l)), the nth element equals l.rotate n.

Русский

Для любого списка l и n, если n < length(cyclicPermutations l), то (cyclicPermutations l).get n = l.rotate n.

LaTeX

$$$ (\text{cyclicPermutations}~l).get~n = l.rotate~n $$$

Lean4

theorem get_cyclicPermutations (l : List α) (n : Fin (length (cyclicPermutations l))) :
    (cyclicPermutations l).get n = l.rotate n := by simp

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

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

Разделы

Аффилиация

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