vecMulVec_cons — Mathlib

English

Let α be a nonunital nonassoc semiring. Then vecMulVec v (vecCons x w) equals the vector whose i-th component is v(i) times the i-th component of vecCons x w.

Русский

Пусть α — неединичное неассоциативное полукольцо. Тогда vecMulVec v (vecCons x w) равен вектору, у которого i-я компонента равна v(i) умножить на i-ю компоненту vecCons x w.

LaTeX

$$$\mathrm{vecMulVec}(v, \mathrm{vecCons}(x,w)) = \mathrm{coe}\;\big(i \mapsto v(i) \cdot (\mathrm{vecCons}(x,w))(i)\big).$$$

Lean4

@[simp]
theorem vecMulVec_cons (v : m' → α) (x : α) (w : Fin n → α) :
    vecMulVec v (vecCons x w) = of fun i => v i • vecCons x w :=
  rfl

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