sub_cons — Mathlib

English

Subtracting a vecCons from a vector yields a vecCons of coordinatewise differences.

Русский

Вычитание vecCons из вектора даёт vecCons разностей по координатам.

LaTeX

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

Lean4

@[simp]
theorem sub_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]

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