rotate'_length — Mathlib

English

For any list l, rotating by its length yields the original list: rotate' l.length = l.

Русский

Для любого списка l вращение на его длину возвращает исходный список: rotate' l.length = l.

LaTeX

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

Lean4

@[simp]
theorem rotate'_length (l : List α) : rotate' l l.length = l := by rw [rotate'_eq_drop_append_take le_rfl]; simp

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