English
The reverse characteristic polynomial of a matrix M is defined as the determinant of 1 minus X times M mapped into polynomials: charpolyRev(M) := det(1 − (X) · M.map C).
Русский
Обратный характеристический многочлен матрицы M определяется как детерминант равенства 1 минус X умножить на отображённую в полиномы матрицу M: charpolyRev(M) = det(1 − X · M.map C).
LaTeX
$$$\\mathrm{charpolyRev}(M) = \\det\\bigl(1 - X \\cdot M\\!\\mapsto\\mathbb{C}\\bigr)$$$
Lean4
/-- The reverse of the characteristic polynomial of a matrix.
It has some advantages over the characteristic polynomial, including the fact that it can be
extended to infinite dimensions (for appropriate operators). In such settings it is known as the
"characteristic power series". -/
def charpolyRev (M : Matrix n n R) : R[X] :=
det (1 - (X : R[X]) • M.map C)
