singleton_eq_rotate_iff — Mathlib

English

Equality with a rotated singleton implies the same singleton: [x] = l.rotate n iff [x] = l.

Русский

Равенство вращенного одиночного списка и другого списка эквивалентно тому, что этот список тоже одиночный: [x] = l.rotate n ⇔ [x] = l.

LaTeX

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

Lean4

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

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