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