rotate_nil — Mathlib

English

Let α be a type. For every n ∈ ℕ, the rotation of the empty list of α by n is the empty list.

Русский

Пусть α — тип. Для любого n ∈ ℕ вращение пустого списка α по операции вращения на n дает пустой список.

LaTeX

$$$\\forall \\alpha \\in \\mathsf{Type},\\ \\forall n \\in \\mathbb{N},\\ ([] : \\mathsf{List}(\\alpha)).rotate\\ n = []$$$

Lean4

@[simp]
theorem rotate_nil (n : ℕ) : ([] : List α).rotate n = [] := by simp [rotate]

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