charmatrix — Mathlib

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

Похожие утверждения