rotate_mod

Mathlib.Data.List.Rotate

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

English

Rotating a list by n is the same as rotating by n modulo its length.

Русский

Поворот списка на n эквивалентен повороту на n по модулю длины списка.

LaTeX

$$$\mathrm{rotate}(l, n) = \mathrm{rotate}(l, n \bmod |l|)$$$

Lean4

theorem rotate_mod (l : List α) (n : ℕ) : l.rotate (n % l.length) = l.rotate n := by simp [rotate]

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

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

Разделы

Аффилиация

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