spectrum_toMatrix' — Mathlib

English

The spectrum is preserved under the matrix-equivalence between endomorphisms and their matrix representations in the isomorphism to matrices.

Русский

Спектр сохраняется при переходе между конечномерными преобразованиями и их матричными представлениями через соответствие матриц.

LaTeX

$$$$ \operatorname{spec}_R(f) = \operatorname{spec}_R(f^{\mathrm{toMatrixAlgEquiv}'}). $$$$

Lean4

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

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