length_rotate' — Mathlib

English

For every list l, the length of l.rotate' n equals the length of l: length(l.rotate' n) = length(l).

Русский

Для каждого списка l длина l.rotate' n равна длине l: length(l.rotate' n) = length(l).

LaTeX

$$$\\forall \\alpha \\in \\mathsf{Type},\\ \\forall l \\in \\mathsf{List}(\\alpha),\\ forall n,\\ \\operatorname{length}(l.rotate' n) = \\operatorname{length}(l)$$$

Lean4

@[simp]
theorem length_rotate' : ∀ (l : List α) (n : ℕ), (l.rotate' n).length = l.length
  | [], _ => by simp
  | _ :: _, 0 => rfl
  | a :: l, n + 1 => by rw [List.rotate', length_rotate' (l ++ [a]) n]; simp

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