English
The characteristic matrix of a matrix M is the matrix tI − M with entries in the polynomial ring, and its determinant is the characteristic polynomial of M.
Русский
Характеристическая матрица матрицы M есть матрица tI − M со значениями в кольце полиномов; её детерминант есть характеристический многочлен M.
LaTeX
$$$\chi_M(t) = \det\big(tI - M\big)$$$
Lean4
/-- The "characteristic matrix" of `M : Matrix n n R` is the matrix of polynomials $t I - M$.
The determinant of this matrix is the characteristic polynomial.
-/
def charmatrix (M : Matrix n n R) : Matrix n n R[X] :=
Matrix.scalar n (X : R[X]) - (C : R →+* R[X]).mapMatrix M