rotate'_length_mul — Mathlib

English

For any list l and natural n, l.rotate' (length(l) · n) = l.

Русский

Для любого списка l и натурального n, l.rotate' (длина(l) · n) = l.

LaTeX

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

Lean4

@[simp]
theorem rotate'_length_mul (l : List α) : ∀ n : ℕ, l.rotate' (l.length * n) = l
  | 0 => by simp
  | n + 1 =>
    calc
      l.rotate' (l.length * (n + 1)) = (l.rotate' (l.length * n)).rotate' (l.rotate' (l.length * n)).length := by
        simp [-rotate'_length, Nat.mul_succ, rotate'_rotate']
      _ = l := by rw [rotate'_length, rotate'_length_mul l n]

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