nil_eq_rotate_iff — Mathlib

English

Let l be a list. For every natural number n, l rotated by n is empty if and only if l is empty; equivalently, the empty list is a rotation of l exactly when l is the empty list.

Русский

Пусть l — список. Для любого натурального числа n поворот списка l на n равен пустому списку тогда и только тогда, когда сам l пуст. Эквивалентно: пустой список является поворотом l тогда и только если l пуст.

LaTeX

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

Lean4

theorem nil_eq_rotate_iff {l : List α} {n : ℕ} : [] = l.rotate n ↔ [] = l := by rw [eq_comm, rotate_eq_nil_iff, eq_comm]

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