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} [DecidableEq n] [Fintype n] [CommRing α] (A B : Matrix n n α) : (Polynomial.X • A.map ⇑Polynomial.C + B.map ⇑Polynomial.C).det.natDegree ≤ Fintype.card n

theorem Polynomial.coeff_det_X_add_C_zero {n : Type u_1} {α : Type u_2} [DecidableEq n] [Fintype n] [CommRing α] (A 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} [DecidableEq n] [Fintype n] [CommRing α] (A B : Matrix n n α) : (Polynomial.X • A.map ⇑Polynomial.C + B.map ⇑Polynomial.C).det.coeff (Fintype.card n) = A.det

theorem Polynomial.leadingCoeff_det_X_one_add_C {n : Type u_1} {α : Type u_2} [DecidableEq n] [Fintype n] [CommRing α] (A : Matrix n n α) : (Polynomial.X • 1 + A.map ⇑Polynomial.C).det.leadingCoeff = 1