isRotated_concat

Mathlib.Data.List.Rotate

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

English

For any l and hd, the list tl ++ [hd] is a rotation of hd :: tl.

Русский

Для любого списка l и головы hd, список tl ++ [hd] является вращением hd :: tl.

LaTeX

$$$ (tl ++ [hd]) \sim_{\mathrm{rot}} (hd :: tl) $$$

Lean4

theorem isRotated_concat (hd : α) (tl : List α) : (tl ++ [hd]) ~r (hd :: tl) :=
  IsRotated.symm ⟨1, by simp⟩

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

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

Разделы

Аффилиация

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