isRotated_append

Mathlib.Data.List.Rotate

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

English

Concatenating two lists and swapping their order yields a rotation: l ++ l' is a rotation of l' ++ l.

Русский

Соединение двух списков с изменением их порядка даёт вращение: l ++ l' — вращение l' ++ l.

LaTeX

$$$ (l ++ l') \sim_{\mathrm{rot}} (l' ++ l) $$$

Lean4

theorem isRotated_append : (l ++ l') ~r (l' ++ l) :=
  ⟨l.length, by simp⟩

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

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

Разделы

Аффилиация

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