removeNth_zero

Mathlib.Data.Fin.Tuple.Basic

URI: https://scilib.ai/kg/mathlib#Fin.removeNth_zero

English

Removing the first entry (index 0) from a tuple f yields tail f.

Русский

Удаление нулевой позиции из кортежа f дает хвост f.

LaTeX

$$removeNth\ 0\ f = tail\ f$$

Lean4

@[simp]
theorem removeNth_zero (f : ∀ i, α i) : removeNth 0 f = tail f := by ext; simp [tail, removeNth]

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

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

Разделы

Аффилиация

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