rotate_eq_singleton_iff — Mathlib

English

Rotation preserves singleton structure: l.rotate n = [x] iff l = [x].

Русский

Поворот сохраняет структуру одиночного элемента: l.rotate n = [x] тогда и только тогда, когда l = [x].

LaTeX

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

Lean4

@[simp]
theorem rotate_eq_singleton_iff {l : List α} {n : ℕ} {x : α} : l.rotate n = [x] ↔ l = [x] := by
  rw [rotate_eq_iff, rotate_singleton]

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