insertNth_zero'

Mathlib.Data.Fin.Tuple.Basic

URI: https://scilib.ai/kg/mathlib#Fin.insertNth_zero'

English

Inserting at position 0 with a function of a constant type yields cons: insertNth 0 x p = cons x p.

Русский

Вставка на нулевой позиции с константным типом функций даёт cons: insertNth 0 x p = cons x p.

LaTeX

$$@insertNth 0 x p = cons x p$$

Lean4

@[simp]
theorem insertNth_zero' (x : β) (p : Fin n → β) : @insertNth _ (fun _ ↦ β) 0 x p = cons x p := by simp [insertNth_zero]

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

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

Разделы

Аффилиация

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