rotate'_cons_succ — Mathlib

English

If a list is formed by consing an element a onto l, then (a :: l).rotate' n.succ = (l ++ [a]).rotate' n.

Русский

Если список образован конструктором cons, добавив элемент a к l, то (a :: l).rotate' (n+1) = (l ++ [a]).rotate' n.

LaTeX

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

Lean4

theorem rotate'_cons_succ (l : List α) (a : α) (n : ℕ) : (a :: l : List α).rotate' n.succ = (l ++ [a]).rotate' n := by
  simp [rotate']

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