# Documentation

Mathlib.LinearAlgebra.Matrix.MvPolynomial

# 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).

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) :
Matrix.map () (MvPolynomial.eval₂ f fun p => A p.fst p.snd) = 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) :
↑(RingHom.mapMatrix (MvPolynomial.eval fun p => A p.fst p.snd)) () = 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) :
↑(AlgHom.mapMatrix (MvPolynomial.aeval fun p => A p.fst p.snd)) () = 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) [] [] [] [] :

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