rotate_zero — Mathlib

English

Let α be a type. For every list l of α, rotating by 0 leaves the list unchanged: l.rotate 0 = l.

Русский

Пусть α — тип. Для каждого списка l из α вращение на 0 оставляет список без изменений: l.rotate 0 = l.

LaTeX

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

Lean4

@[simp]
theorem rotate_zero (l : List α) : l.rotate 0 = l := by simp [rotate]

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