rotate_length_mul — Mathlib

English

Rotating by length(l) times n yields the original list: l.rotate (length(l) · n) = l.

Русский

Вращение на length(l) · n даёт исходный список: l.rotate (length(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 := by
  rw [rotate_eq_rotate', rotate'_length_mul]

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