spectrum_toEuclideanLin — Mathlib

English

The spectrum of a matrix is preserved under a change of basis; i.e., the spectrum of A equals the spectrum of its Euclidean-Lin representation.

Русский

Спектр матрицы сохраняется при переходе к другой базисной системе; то есть спектр A равен спектру её представления в евклидовой системе координат.

LaTeX

$$$\operatorname{Spec}_{\mathbb{K}}(\mathrm{toEuclideanLin}(A)) = \operatorname{Spec}_{\mathbb{K}}(A)$$$

Lean4

/-- The spectrum of a matrix `A` coincides with the spectrum of `toEuclideanLin A`. -/
theorem spectrum_toEuclideanLin [DecidableEq n] : spectrum 𝕜 (toEuclideanLin A) = spectrum 𝕜 A :=
  AlgEquiv.spectrum_eq (Matrix.toLinAlgEquiv (PiLp.basisFun 2 𝕜 n)) _

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