# 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 unique variable.

## Tags #

matrix determinant, multivariate polynomial

noncomputable def Matrix.mvPolynomialX (m : Type u_1) (n : Type u_2) (R : Type u_3) [] :
Matrix m n (MvPolynomial (m × n) R)

The matrix with variable X (i,j) at location (i,j).

Equations
Instances For
@[simp]
theorem Matrix.mvPolynomialX_apply (m : Type u_1) (n : Type u_2) (R : Type u_3) [] (i : m) (j : n) :
theorem Matrix.mvPolynomialX_map_eval₂ {m : Type u_1} {n : Type u_2} {R : Type u_3} {S : Type u_4} [] [] (f : R →+* S) (A : Matrix m n S) :
().map (MvPolynomial.eval₂ f fun (p : m × n) => A p.1 p.2) = A

Any matrix A can be expressed as the evaluation of Matrix.mvPolynomialX.

This is of particular use when MvPolynomial (m × n) R is an integral domain but S is not, as if the MvPolynomial.eval₂ can be pulled to the outside of a goal, it can be solved in under cancellative assumptions.

theorem Matrix.mvPolynomialX_mapMatrix_eval {m : Type u_1} {R : Type u_3} [] [] [] (A : Matrix m m R) :
(MvPolynomial.eval fun (p : m × m) => A p.1 p.2).mapMatrix () = A

A variant of Matrix.mvPolynomialX_map_eval₂ with a bundled RingHom on the LHS.

theorem Matrix.mvPolynomialX_mapMatrix_aeval {m : Type u_1} (R : Type u_3) {S : Type u_4} [] [] [] [] [Algebra R S] (A : Matrix m m S) :
(MvPolynomial.aeval fun (p : m × m) => A p.1 p.2).mapMatrix () = A

A variant of Matrix.mvPolynomialX_map_eval₂ with a bundled AlgHom on the LHS.

theorem Matrix.det_mvPolynomialX_ne_zero (m : Type u_1) (R : Type u_3) [] [] [] [] :
().det 0

In a nontrivial ring, Matrix.mvPolynomialX m m R has non-zero determinant.