spectrum_toMatrix — Mathlib

English

The spectrum of a linear map equals the spectrum of its matrix representation in any basis.

Русский

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

LaTeX

$$$$ \operatorname{spec}_R(f) = \operatorname{spec}_R(f^{\mathrm{toMatrix}}(b,b)). $$$$

Lean4

@[simp]
theorem _root_.LinearMap.spectrum_toMatrix (f : M →ₗ[R] M) (b : Basis n R M) :
    spectrum R (f.toMatrix b b) = spectrum R f :=
  AlgEquiv.spectrum_eq (LinearMap.toMatrixAlgEquiv b) f

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