eraseIdx_val

Mathlib.Data.Vector.Basic

URI: https://scilib.ai/kg/mathlib#List.Vector.eraseIdx_val

English

The value of (eraseIdx i v).val equals v.val.eraseIdx i.

Русский

Значение (eraseIdx i v).val равно v.val.eraseIdx i.

LaTeX

$$$ (eraseIdx\\ i\\ v).val = v.val.eraseIdx i $$$

Lean4

@[simp]
theorem eraseIdx_val {i : Fin n} : ∀ {v : Vector α n}, (eraseIdx i v).val = v.val.eraseIdx i
  | _ => rfl

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

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

Разделы

Аффилиация

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