cons_vecMulVec — Mathlib

English

Let α be a nonunital nonassoc semiring. Then vecMulVec (vecCons x v) w = of fun i => v i • vecCons x w.

Русский

Пусть α — неединичное неассоциативное полукольцо. Тогда vecMulVec (vecCons x v) w = of fun i => v i • vecCons x w.

LaTeX

$$$\mathrm{vecMulVec}(\mathrm{vecCons}(x,v), w) = \mathrm{of}\, (\lambda i. v(i) \cdot \mathrm{vecCons}(x,w)(i)).$$$

Lean4

@[simp]
theorem cons_vecMulVec (x : α) (v : Fin m → α) (w : n' → α) :
    vecMulVec (vecCons x v) w = vecCons (x • w) (vecMulVec v w) :=
  by
  ext i
  refine Fin.cases ?_ ?_ i <;> simp [vecMulVec]

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