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

theorem Polynomial.coeff_det_X_add_C_zero {n : Type u_1} {α : Type u_2} [DecidableEq n] [Fintype n] [CommRing α] (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 = Matrix.det B

theorem Polynomial.coeff_det_X_add_C_card {n : Type u_1} {α : Type u_2} [DecidableEq n] [Fintype n] [CommRing α] (A : Matrix n n α) (B : Matrix n n α) : Polynomial.coeff (Matrix.det (Polynomial.X • Matrix.map A ↑Polynomial.C + Matrix.map B ↑Polynomial.C)) (Fintype.card n) = Matrix.det A

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.leadingCoeff (Matrix.det (Polynomial.X • 1 + Matrix.map A ↑Polynomial.C)) = 1