rotate_eq_drop_append_take_mod — Mathlib

English

Rotation with modulus: l.rotate' (n mod length(l)) = l.rotate' n, i.e., rotation is periodic with period length(l).

Русский

Вращение с модулем: l.rotate' (n mod length(l)) = l.rotate' n, то есть вращение периодично с периодом length(l).

LaTeX

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

Lean4

theorem rotate_eq_drop_append_take_mod {l : List α} {n : ℕ} :
    l.rotate n = l.drop (n % l.length) ++ l.take (n % l.length) :=
  by
  rcases l.length.zero_le.eq_or_lt with hl | hl
  · simp [eq_nil_of_length_eq_zero hl.symm]
  rw [← rotate_eq_drop_append_take (n.mod_lt hl).le, rotate_mod]

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