Metamath Proof Explorer


Table of Contents - 11.2.3. The matrix algebra

The main result of this subsection are the theorems showing that is a ring (see matring) and an associative algebra (see matassa). Additionally, theorems for the identity matrix and transposed matrices are provided.

  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