charpoly_mulVecLin — Mathlib

English

For a square matrix A, the endomorphism A.mulVecLin on the vector space R^n has the same characteristic polynomial as A itself: χ_{A.mulVecLin} = χ_A.

Русский

Для квадратной матрицы A линейное преобразование A.mulVecLin имеет тот же характеристический многочлен, что и сама матрица: χ_{A.mulVecLin} = χ_A.

LaTeX

$$$\operatorname{charpoly}(A^{mulVecLin}) = \operatorname{charpoly}(A)$$$

Lean4

@[simp]
theorem charpoly_mulVecLin (A : Matrix n n R) : A.mulVecLin.charpoly = A.charpoly :=
  charpoly_toLin' A

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