Metamath Proof Explorer


Table of Contents - 11.4.2. Constant polynomial matrices

A constant polynomial matrix is a polynomial matrix whose elements are constant polynomials, i.e. polynomials with no indeterminates. Constant polynomials are obtained by "lifting" a "scalar" (i.e. an element of the underlying ring) into the polynomial ring/algebra by a "scalar injection", i.e. applying the "algebra scalar injection function" (see df-ascl) to a scalar : . In an analogous way, constant polynomial matrices (over the ring ) are obtained by "lifting" matrices over the ring by the function (see df-mat2pmat), called "matrix transformation" in the following.

In this section it is shown that the set of constant polynomial x matrices over the ring is a subring of the ring of polynomial x matrices over the ring (cpmatsrgpmat) and that is a ring isomorphism between the ring of matrices over a ring and the ring of constant polynomial matrices over the ring (see m2cpmrngiso). By this, it is shown that the ring of matrices over a commutative ring is isomorphic to the ring of scalar matrices over the same ring, see matcpmric. Finally , the transformation of a constant polynomial matrix into a matrix, is the inverse function of the matrix transformation , see m2cpminv.

  1. ccpmat
  2. cmat2pmat
  3. ccpmat2mat
  4. df-cpmat
  5. df-mat2pmat
  6. df-cpmat2mat
  7. cpmat
  8. cpmatpmat
  9. cpmatel
  10. cpmatelimp
  11. cpmatel2
  12. cpmatelimp2
  13. 1elcpmat
  14. cpmatacl
  15. cpmatinvcl
  16. cpmatmcllem
  17. cpmatmcl
  18. cpmatsubgpmat
  19. cpmatsrgpmat
  20. 0elcpmat
  21. mat2pmatfval
  22. mat2pmatval
  23. mat2pmatvalel
  24. mat2pmatbas
  25. mat2pmatbas0
  26. mat2pmatf
  27. mat2pmatf1
  28. mat2pmatghm
  29. mat2pmatmul
  30. mat2pmat1
  31. mat2pmatmhm
  32. mat2pmatrhm
  33. mat2pmatlin
  34. 0mat2pmat
  35. idmatidpmat
  36. d0mat2pmat
  37. d1mat2pmat
  38. mat2pmatscmxcl
  39. m2cpm
  40. m2cpmf
  41. m2cpmf1
  42. m2cpmghm
  43. m2cpmmhm
  44. m2cpmrhm
  45. m2pmfzmap
  46. m2pmfzgsumcl
  47. cpm2mfval
  48. cpm2mval
  49. cpm2mvalel
  50. cpm2mf
  51. m2cpminvid
  52. m2cpminvid2lem
  53. m2cpminvid2
  54. m2cpmfo
  55. m2cpmf1o
  56. m2cpmrngiso
  57. matcpmric
  58. m2cpminv
  59. m2cpminv0