vecMul_vecMul — Mathlib

English

For finite semiring, the vector-matrix-vector associativity holds: vᵥ* M ᵥ* N = vᵥ*(M*N).

Русский

Для конечного полууравнения выполняется ассоциативность: vᵥ* M ᵥ* N = vᵥ*(M*N).

LaTeX

$$$\\text{vecMul}\\,(\\text{vecMul}\\, v\\, M)\\, N = \\text{vecMul}\\, v\\, (M \\cdot N).$$$

Lean4

@[simp]
theorem vecMul_vecMul [Fintype n] [Fintype m] (v : m → α) (M : Matrix m n α) (N : Matrix n o α) :
    v ᵥ* M ᵥ* N = v ᵥ* (M * N) := by
  ext
  apply dotProduct_assoc

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