rotate_singleton

Mathlib.Data.List.Rotate

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

English

Rotating a singleton list leaves it unchanged: for any x and any n, [x].rotate n = [x].

Русский

Поворот списка-одиночки оставляет его без изменений: для любого x и любого n, [x].rotate n = [x].

LaTeX

$$$\forall x:\\alpha, \\forall n:\\mathbb{N}, [x].rotate n = [x]$$$

Lean4

@[simp]
theorem rotate_singleton (x : α) (n : ℕ) : [x].rotate n = [x] :=
  rotate_replicate x 1 n

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

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

Разделы

Аффилиация

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