spectrum_toLin — Mathlib

English

The spectrum of a matrix and the spectrum of the corresponding linear map given by the matrix representation are equal.

Русский

Спектр матрицы и спектр соответствующего линейного отображения, заданного матрицей, совпадают.

LaTeX

$$$$ \operatorname{spec}_R(A) = \operatorname{spec}_R(A^{\toLin\,b\,b}). $$$$

Lean4

@[simp]
theorem spectrum_toLin (A : Matrix n n R) (b : Basis n R M) : spectrum R (A.toLin b b) = spectrum R A :=
  AlgEquiv.spectrum_eq (Matrix.toLinAlgEquiv b) A

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