spectrum_toLin' — Mathlib

English

The spectrum of a matrix and the spectrum of its linear map form via toLin' are identical.

Русский

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

LaTeX

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

Lean4

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

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