rotate'_rotate' — Mathlib

English

For any list l and natural numbers n,m, (l.rotate' n).rotate' m = l.rotate' (n + m).

Русский

Для любого списка l и натуральных чисел n, m, выполняется (l.rotate' n).rotate' m = l.rotate' (n + m).

LaTeX

$$$\\forall \\alpha \\in \\mathsf{Type},\\ \\forall l \\in \\mathsf{List}(\\alpha),\\forall n,m \in \\mathbb{N},\\ (l.rotate' n).rotate' m = l.rotate' (n + m)$$$

Lean4

theorem rotate'_rotate' : ∀ (l : List α) (n m : ℕ), (l.rotate' n).rotate' m = l.rotate' (n + m)
  | a :: l, 0, m => by simp
  | [], n, m => by simp
  | a :: l, n + 1, m => by
    rw [rotate'_cons_succ, rotate'_rotate' _ n, Nat.add_right_comm, ← rotate'_cons_succ, Nat.succ_eq_add_one]

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