insert_fz

Mathlib.Data.Vector3

URI: https://scilib.ai/kg/mathlib#Vector3.insert_fz

English

Inserting at the front yields the cons vector: insert(a, v, fz) = a :: v.

Русский

Вставка в начало даёт вектор cons: insert(a, v, fz) = a :: v.

LaTeX

$$$ \mathrm{insert}(a,v,\mathrm{fz}) = a :: v. $$$

Lean4

@[simp]
theorem insert_fz (a : α) (v : Vector3 α n) : insert a v fz = a :: v := by
  refine funext fun j => j.cases' ?_ ?_ <;> intros <;> rfl

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

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

Разделы

Аффилиация

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