# Documentation

Mathlib.LinearAlgebra.Matrix.Polynomial

# Matrices of polynomials and polynomials of matrices #

In this file, we prove results about matrices over a polynomial ring. In particular, we give results about the polynomial given by det (t * I + A).

## References #

• "The trace Cayley-Hamilton theorem" by Darij Grinberg, Section 5.3

## Tags #

matrix determinant, polynomial

theorem Polynomial.natDegree_det_X_add_C_le {n : Type u_1} {α : Type u_2} [] [] [] (A : Matrix n n α) (B : Matrix n n α) :
Polynomial.natDegree (Matrix.det (Polynomial.X Matrix.map A Polynomial.C + Matrix.map B Polynomial.C))
theorem Polynomial.coeff_det_X_add_C_zero {n : Type u_1} {α : Type u_2} [] [] [] (A : Matrix n n α) (B : Matrix n n α) :
Polynomial.coeff (Matrix.det (Polynomial.X Matrix.map A Polynomial.C + Matrix.map B Polynomial.C)) 0 =
theorem Polynomial.coeff_det_X_add_C_card {n : Type u_1} {α : Type u_2} [] [] [] (A : Matrix n n α) (B : Matrix n n α) :
Polynomial.coeff (Matrix.det (Polynomial.X Matrix.map A Polynomial.C + Matrix.map B Polynomial.C)) () =
theorem Polynomial.leadingCoeff_det_X_one_add_C {n : Type u_1} {α : Type u_2} [] [] [] (A : Matrix n n α) :
Polynomial.leadingCoeff (Matrix.det (Polynomial.X 1 + Matrix.map A Polynomial.C)) = 1