charpoly — Mathlib

English

The characteristic polynomial χ_M of a matrix M is defined as the determinant of the matrix tI − M, i.e., χ_M = det(tI − M).

Русский

Характеристический многочлен χ_M матрицы M определяется как детерминант матрицы tI − M, то есть χ_M = det(tI − M).

LaTeX

$$$\operatorname{charpoly}(M) = \det(tI - M)$$$

Lean4

/-- The characteristic polynomial of a matrix `M` is given by $\det (t I - M)$. -/
def charpoly (M : Matrix n n R) : R[X] :=
  (charmatrix M).det

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