Matrices of polynomials and polynomials of matrices #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.
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.nat_degree_det_X_add_C_le
{n : Type u_1}
{α : Type u_2}
[decidable_eq n]
[fintype n]
[comm_ring α]
(A B : matrix n n α) :
(polynomial.X • A.map ⇑polynomial.C + B.map ⇑polynomial.C).det.nat_degree ≤ fintype.card n
theorem
polynomial.coeff_det_X_add_C_zero
{n : Type u_1}
{α : Type u_2}
[decidable_eq n]
[fintype n]
[comm_ring α]
(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}
[decidable_eq n]
[fintype n]
[comm_ring α]
(A B : matrix n n α) :
(polynomial.X • A.map ⇑polynomial.C + B.map ⇑polynomial.C).det.coeff (fintype.card n) = A.det
theorem
polynomial.leading_coeff_det_X_one_add_C
{n : Type u_1}
{α : Type u_2}
[decidable_eq n]
[fintype n]
[comm_ring α]
(A : matrix n n α) :
(polynomial.X • 1 + A.map ⇑polynomial.C).det.leading_coeff = 1