charpoly_toLin' — Mathlib

English

Let A be a square matrix over a commutative ring R and b a basis of a finitely generated free module M. Then the characteristic polynomial of the linear map A.toLin b b is equal to the characteristic polynomial of the matrix A.

Русский

Пусть A — квадратная матрица над кольцом R, а b — базис модуля M. Тогда характеристический многочлен линейного отображения A.toLin b b равен характеристическому многочлену самой матрицы A.

LaTeX

$$$\operatorname{charpoly}(A^{toLin}\,b\,b) = A\!:\operatorname{charpoly}$$$

Lean4

@[simp]
theorem charpoly_toLin' (A : Matrix n n R) : A.toLin'.charpoly = A.charpoly := by
  rw [← Matrix.toLin_eq_toLin', charpoly_toLin]

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