insertNth_last'

Mathlib.Data.Fin.Tuple.Basic

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

English

A simplified form: (last n).insertNth x p = snoc p x.

Русский

Упрощенная форма: (last n).insertNth x p = snoc p x.

LaTeX

$$$(Fin.last\ n).insertNth x p = \mathrm{snoc}\; p\; x$$

Lean4

@[simp]
theorem insertNth_last' (x : β) (p : Fin n → β) : @insertNth _ (fun _ ↦ β) (last n) x p = snoc p x := by
  simp [insertNth_last]

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

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

Разделы

Аффилиация

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