cons_sub — Mathlib

English

Subtracting a tail from a vecCons on the right distributes as vecCons (x - head) (v - tail).

Русский

Вычитание хвоста vecCons справа распадается на vecCons (x - голова) (v - хвост).

LaTeX

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

Lean4

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

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