add_cons — Mathlib

English

The sum of a general vector v with a vecCons y w equals vecCons (head v + y) (tail v + w).

Русский

Сумма произвольного вектора v и vecCons y w равна vecCons (head v + y) (tail v + w).

LaTeX

$$$ v + \mathrm{vecCons} y w = \mathrm{vecCons}(\mathrm{vecHead} v + y) (\mathrm{vecTail} v + w) $$$

Lean4

@[simp]
theorem add_cons (v : Fin n.succ → α) (y : α) (w : Fin n → α) :
    v + vecCons y w = vecCons (vecHead v + y) (vecTail v + w) := by ext i;
  refine i.cases ?_ ?_ <;> simp [vecHead, vecTail]

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