Metamath Proof Explorer


Table of Contents - 11.2.5. The subalgebras of diagonal and scalar matrices

According to Wikipedia ("Diagonal Matrix", 8-Dec-2019, https://en.wikipedia.org/wiki/Diagonal_matrix): "In linear algebra, a diagonal matrix is a matrix in which the entries outside the main diagonal are all zero; the term usually refers to square matrices." The diagonal matrices are mentioned in [Lang] p. 576, but without giving them a dedicated definition. Furthermore, "A diagonal matrix with all its main diagonal entries equal is a scalar matrix, that is, a scalar multiple of the identity matrix . Its effect on a vector is scalar multiplication by [see scmatscm!]". The scalar multiples of the identity matrix are mentioned in [Lang] p. 504, but without giving them a special name.

The main results of this subsection are the definitions of the sets of diagonal and scalar matrices (df-dmat and df-scmat), basic properties of (elements of) these sets, and theorems showing that the diagonal matrices are a subring of the ring of square matrices (dmatsrng), that the scalar matrices are a subring of the ring of square matrices (scmatsrng), that the scalar matrices are a subring of the ring of diagonal matrices (scmatsrng1) and that the ring of scalar matrices (over a commutative ring) is a commutative ring (scmatcrng).

  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