Matrices of multivariate polynomials #
In this file, we prove results about matrices over an mv_polynomial ring.
In particular, we provide
Matrix.mvPolynomialX which associates every entry of a matrix with a
matrix determinant, multivariate polynomial
A can be expressed as the evaluation of
This is of particular use when
MvPolynomial (m × n) R is an integral domain but
not, as if the
MvPolynomial.eval₂ can be pulled to the outside of a goal, it can be solved in
under cancellative assumptions.