Metamath Proof Explorer


Table of Contents - 11.2. Matrices

According to Wikipedia ("Matrix (mathemetics)", 02-Apr-2019, https://en.wikipedia.org/wiki/Matrix_(mathematics)) "A matrix is a rectangular array of numbers or other mathematical objects for which operations such as addition and multiplication are defined. Most commonly, a matrix over a field F is a rectangular array of scalars each of which is a member of F. The numbers, symbols or expressions in the matrix are called its entries or its elements. The horizontal and vertical lines of entries in a matrix are called rows and columns, respectively.", and in the definition of [Lang] p. 503 "By an m x n matrix in [a commutative ring] R one means a doubly indexed family of elements of R, (aij), (i= 1,..., m and j = 1,... n) ... We call the elements aij the coefficients or components of the matrix. A 1 x n matrix is called a row vector (of dimension, or size, n) and a m x 1 matrix is called a column vector (of dimension, or size, m). In general, we say that (m,n) is the size of the matrix, ...". In contrast to these definitions, we denote any free module over a (not necessarily commutative) ring (in the meaning of df-frlm) with a Cartesian product as index set as "matrix". The two sets of the Cartesian product even need neither to be ordered or a range of (nonnegative/positive) integers nor finite. By this, the addition and scalar multiplication for matrices correspond to the addition (see frlmplusgval) and scalar multiplication (see frlmvscafval) for free modules. Actually, there isn't a definition for (arbitrary) matrices: Even the (general) matrix multiplication can be defined using functions from Cartesian products into a ring (which are elements of the base set of free modules), see df-mamu. By this, a statement like "Then the set of m x n matrices in R is a module (i.e., an R-module)" as in [Lang] p. 504 follows immediately from frlmlmod.

However, for square matrices there is the definition df-mat, defining the algebras of square matrices (of the same size over the same ring), extending the structure of the corresponding free module by the matrix multiplication as ring multiplication.

A "usual" matrix (aij), (i= 1,..., m and j = 1,... n) would be represented as element of (the base set of) , and a square matrix (aij), (i= 1,..., n and j = 1,... n) would be represented as element of (the base set of) .

Finally, it should be mentioned that our definitions of matrices include the zero-dimensional cases, which is excluded in the definition of many authors, e.g. in [Lang] p. 503. It is shown in mat0dimbas0 that the empty set is the sole zero-dimensional matrix (also called "empty matrix", see Wikipedia https://en.wikipedia.org/wiki/Matrix_(mathematics)#Empty_matrices). The determinant is also defined for such an empty matrix, see mdet0pr.

  1. The matrix multiplication
    1. cmmul
    2. df-mamu
    3. mamufval
    4. mamuval
    5. mamufv
    6. mamudm
    7. mamufacex
    8. mamures
    9. mndvcl
    10. mndvass
    11. mndvlid
    12. mndvrid
    13. grpvlinv
    14. grpvrinv
    15. mhmvlin
    16. ringvcl
    17. mamucl
    18. mamuass
    19. mamudi
    20. mamudir
    21. mamuvs1
    22. mamuvs2
  2. Square matrices
    1. cmat
    2. df-mat
    3. matbas0pc
    4. matbas0
    5. matval
    6. matrcl
    7. matbas
    8. matplusg
    9. matsca
    10. matvsca
    11. mat0
    12. matinvg
    13. mat0op
    14. matsca2
    15. matbas2
    16. matbas2i
    17. matbas2d
    18. eqmat
    19. matecl
    20. matecld
    21. matplusg2
    22. matvsca2
    23. matlmod
    24. matgrp
    25. matvscl
    26. matsubg
    27. matplusgcell
    28. matsubgcell
    29. matinvgcell
    30. matvscacell
    31. matgsum
  3. The matrix algebra
    1. matmulr
    2. mamumat1cl
    3. mat1comp
    4. mamulid
    5. mamurid
    6. matring
    7. matassa
    8. matmulcell
    9. mpomatmul
    10. mat1
    11. mat1ov
    12. mat1bas
    13. matsc
    14. ofco2
    15. oftpos
    16. mattposcl
    17. mattpostpos
    18. mattposvs
    19. mattpos1
    20. tposmap
    21. mamutpos
    22. mattposm
    23. matgsumcl
    24. madetsumid
    25. matepmcl
    26. matepm2cl
    27. madetsmelbas
    28. madetsmelbas2
  4. Matrices of dimension 0 and 1
    1. mat0dimbas0
    2. mat0dim0
    3. mat0dimid
    4. mat0dimscm
    5. mat0dimcrng
    6. mat1dimelbas
    7. mat1dimbas
    8. mat1dim0
    9. mat1dimid
    10. mat1dimscm
    11. mat1dimmul
    12. mat1dimcrng
    13. mat1f1o
    14. mat1rhmval
    15. mat1rhmelval
    16. mat1rhmcl
    17. mat1f
    18. mat1ghm
    19. mat1mhm
    20. mat1rhm
    21. mat1rngiso
    22. mat1ric
  5. The subalgebras of diagonal and scalar matrices
    1. cdmat
    2. cscmat
    3. df-dmat
    4. df-scmat
    5. dmatval
    6. dmatel
    7. dmatmat
    8. dmatid
    9. dmatelnd
    10. dmatmul
    11. dmatsubcl
    12. dmatsgrp
    13. dmatmulcl
    14. dmatsrng
    15. dmatcrng
    16. dmatscmcl
    17. scmatval
    18. scmatel
    19. scmatscmid
    20. scmatscmide
    21. scmatscmiddistr
    22. scmatmat
    23. scmate
    24. scmatmats
    25. scmateALT
    26. scmatscm
    27. scmatid
    28. scmatdmat
    29. scmataddcl
    30. scmatsubcl
    31. scmatmulcl
    32. scmatsgrp
    33. scmatsrng
    34. scmatcrng
    35. scmatsgrp1
    36. scmatsrng1
    37. smatvscl
    38. scmatlss
    39. scmatstrbas
    40. scmatrhmval
    41. scmatrhmcl
    42. scmatf
    43. scmatfo
    44. scmatf1
    45. scmatf1o
    46. scmatghm
    47. scmatmhm
    48. scmatrhm
    49. scmatrngiso
    50. scmatric
    51. mat0scmat
    52. mat1scmat
  6. Multiplication of a matrix with a "column vector"
    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
  7. Replacement functions for a square matrix
    1. cmarrep
    2. cmatrepV
    3. df-marrep
    4. df-marepv
    5. marrepfval
    6. marrepval0
    7. marrepval
    8. marrepeval
    9. marrepcl
    10. marepvfval
    11. marepvval0
    12. marepvval
    13. marepveval
    14. marepvcl
    15. ma1repvcl
    16. ma1repveval
    17. mulmarep1el
    18. mulmarep1gsum1
    19. mulmarep1gsum2
    20. 1marepvmarrepid
  8. Submatrices
    1. csubma
    2. df-subma
    3. submabas
    4. submafval
    5. submaval0
    6. submaval
    7. submaeval
    8. 1marepvsma1