mathlib3 documentation


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 #

Tags #

matrix determinant, polynomial