cons_add — Mathlib

English

Adding a scalar to a vecCons and the tail to the tail distributes as vecCons (head+scalar) (tail+tail).

Русский

Сложение vecCons с другой векторной частью распределяется так: vecCons x v + w = vecCons (vecHead v + y) (vecTail v + w).

LaTeX

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

Lean4

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

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