getI_zero_eq_headI

Mathlib.Data.List.GetD

URI: https://scilib.ai/kg/mathlib#List.getI_zero_eq_headI

English

The first element of a list equals its head element.

Русский

Первый элемент списка равен его первой головой.

LaTeX

$$$$ l.getI 0 = l.headI. $$$$

Lean4

theorem getI_zero_eq_headI : l.getI 0 = l.headI := by cases l <;> rfl

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

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

Разделы

Аффилиация

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