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.X • A.map ⇑Polynomial.C + B.map ⇑Polynomial.C).det.natDegree ≤ Fintype.card n
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.X • A.map ⇑Polynomial.C + B.map ⇑Polynomial.C).det.coeff (Fintype.card n) = A.det