# 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.X A.map Polynomial.C + B.map Polynomial.C).det.natDegree
theorem Polynomial.coeff_det_X_add_C_zero {n : Type u_1} {α : Type u_2} [] [] [] (A : Matrix n n α) (B : Matrix n n α) :
(Polynomial.X A.map Polynomial.C + B.map Polynomial.C).det.coeff 0 = B.det
theorem Polynomial.coeff_det_X_add_C_card {n : Type u_1} {α : Type u_2} [] [] [] (A : Matrix n n α) (B : Matrix n n α) :
(Polynomial.X A.map Polynomial.C + B.map Polynomial.C).det.coeff () = A.det
theorem Polynomial.leadingCoeff_det_X_one_add_C {n : Type u_1} {α : Type u_2} [] [] [] (A : Matrix n n α) :
(Polynomial.X 1 + A.map Polynomial.C).det.leadingCoeff = 1