Metamath Proof Explorer

Table of Contents - 11.2.6. Multiplication of a matrix with a "column vector"

The module of -dimensional "column vectors" over a ring is the -dimensional free module over a ring , which is the product of -many copies of the ring with componentwise addition and multiplication. Although a "column vector" could also be defined as n x 1 -matrix (according to Wikipedia "Row and column vectors", 22-Feb-2019, "In linear algebra, a column vector [... ] is an m x 1 matrix, that is, a matrix consisting of a single column of m elements"), which would allow for using the matrix multiplication df-mamu for multiplying a matrix with a column vector, it seems more natural to use the definition of a free (left) module, avoiding to provide a singleton as -dimensional index set for the column, and to introduce a new operator df-mvmul for the multiplication of a matrix with a column vector. In most cases, it is sufficient to regard members of as "column vectors", because is the base set of , see frlmbasmap. See also the statements in [Lang] p. 508.

  1. cmvmul
  2. df-mvmul
  3. mvmulfval
  4. mvmulval
  5. mvmulfv
  6. mavmulval
  7. mavmulfv
  8. mavmulcl
  9. 1mavmul
  10. mavmulass
  11. mavmuldm
  12. mavmulsolcl
  13. mavmul0
  14. mavmul0g
  15. mvmumamul1
  16. mavmumamul1