isRotated_singleton_iff'

Mathlib.Data.List.Rotate

URI: https://scilib.ai/kg/mathlib#List.isRotated_singleton_iff'

English

A singleton list [x] is a rotation of l iff l is the singleton [x].

Русский

Одноэлементный список [x] является вращением l тогда и только тогда, когда l является одноэлементным [x].

LaTeX

$$$ [x] \sim_{\mathrm{rot}} l \iff [x] = l $$$

Lean4

@[simp]
theorem isRotated_singleton_iff' {x : α} : [x] ~r l ↔ [x] = l := by
  rw [isRotated_comm, isRotated_singleton_iff, eq_comm]

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

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

Разделы

Аффилиация

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