rotate_cons_succ — Mathlib

English

For any list l and element a, (a :: l).rotate (n + 1) equals (l ++ [a]).rotate n.

Русский

Для любого списка l и элемента a, (a :: l).rotate (n + 1) равно (l ++ [a]).rotate n.

LaTeX

$$$\\forall \\alpha \\in \\mathsf{Type},\\ \\forall l \\in \\mathsf{List}(\\alpha),\\forall a \\in \\alpha,\\ (a :: l).rotate (n + 1) = (l ++ [a]).rotate n$$$

Lean4

@[simp]
theorem rotate_cons_succ (l : List α) (a : α) (n : ℕ) : (a :: l : List α).rotate (n + 1) = (l ++ [a]).rotate n := by
  rw [rotate_eq_rotate', rotate_eq_rotate', rotate'_cons_succ]

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