English
For a matrix A with entries in R and a basis b of the free module M, the characteristic polynomial of the linear map A.toLin b b equals the characteristic polynomial of the matrix A itself. This translates a matrix representation’s charpoly back to the abstract endomorphism charpoly.
Русский
Для матрицы A над R и базиса b свободного модуля M характеристический многочлен линейного отображения A.toLin b b совпадает с характеристическим многочленом самой матрицы A.
LaTeX
$$$\operatorname{charpoly}(A^{toLin}\,b\,b) = \operatorname{charpoly}(A)$$$
Lean4
@[simp]
theorem charpoly_toLin (A : Matrix n n R) (b : Basis n R M) : (A.toLin b b).charpoly = A.charpoly := by
simp [← LinearMap.charpoly_toMatrix (A.toLin b b) b]
