rotate_eq_nil_iff — Mathlib

English

For every finite list l and every natural number n, the rotation l rotated by n equals the empty list if and only if l is empty.

Русский

Для любого конечного списка L и любого натурального числа n поворот списка L на n позиций даёт пустой список тогда и только тогда, когда сам список пуст.

LaTeX

$$$l.rotate n = [] \\iff l = []$$$

Lean4

@[simp]
theorem rotate_eq_nil_iff {l : List α} {n : ℕ} : l.rotate n = [] ↔ l = [] := by
  induction n generalizing l with
  | zero => simp
  | succ n hn =>
    rcases l with - | ⟨hd, tl⟩
    · simp
    · simp [rotate_cons_succ, hn]

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