rotate_rotate — Mathlib

English

Rotating by n and then by m is the same as rotating by n + m: (l.rotate n).rotate m = l.rotate (n + m).

Русский

Постфакторное вращение на n затем на m эквивалентно вращению на 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) := by
  rw [rotate_eq_rotate', rotate_eq_rotate', rotate_eq_rotate', rotate'_rotate']

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