Metamath Proof Explorer


Table of Contents - 11.4.3. Collecting coefficients of polynomial matrices

In this section, the decomposition of polynomial matrices into (polynomial) multiples of constant (polynomial) matrices is prepared by collecting the coefficients of a polynomial matrix which belong to the same power of the polynomial variable. Such a collection is given by the function (see df-decpmat), which maps a polynomial matrix to a constant matrix consisting of the coefficients of the scaled monomials , i.e. the coefficients belonging to the k-th power of the polynomial variable , of each entry in the polynomial matrix . The resulting decomposition is provided by theorem pmatcollpw.

  1. cdecpmat
  2. df-decpmat
  3. decpmatval0
  4. decpmatval
  5. decpmate
  6. decpmatcl
  7. decpmataa0
  8. decpmatfsupp
  9. decpmatid
  10. decpmatmullem
  11. decpmatmul
  12. decpmatmulsumfsupp
  13. pmatcollpw1lem1
  14. pmatcollpw1lem2
  15. pmatcollpw1
  16. pmatcollpw2lem
  17. pmatcollpw2
  18. monmatcollpw
  19. pmatcollpwlem
  20. pmatcollpw
  21. pmatcollpwfi
  22. pmatcollpw3lem
  23. pmatcollpw3
  24. pmatcollpw3fi
  25. pmatcollpw3fi1lem1
  26. pmatcollpw3fi1lem2
  27. pmatcollpw3fi1
  28. pmatcollpwscmatlem1
  29. pmatcollpwscmatlem2
  30. pmatcollpwscmat