mulVec_mulVec — Mathlib

English

Let M be an m×n matrix, N an n×o matrix, and v a column vector in α^o. Then applying N to v and then M gives the same result as applying the product M N to v; i.e. M(Nv) = (MN)v.

Русский

Пусть M — матрица размером m×n, N — матрица размером n×o, и v — вектор в α^o. Тогда сначала применяем N к v, затем M, что эквивалентно применению произведения M N к v; то есть M(Nv) = (MN)v.

LaTeX

$$$(M N) v = M (N v)$$$

Lean4

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

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