rotate'_nil

Mathlib.Data.List.Rotate

URI: https://scilib.ai/kg/mathlib#List.rotate'_nil

English

Let α be a type. The rotated empty list remains empty for the rotate' operation: [] .rotate' n = [].

Русский

Пусть α — тип. Пустой список при операции rotate' остаётся пустым: [] .rotate' n = [].

LaTeX

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

Lean4

theorem rotate'_nil (n : ℕ) : ([] : List α).rotate' n = [] := by simp

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru