Eigenvectors of matrices and the spectrum

Mathlib identifies the spectrum of a square matrix with that of the endomorphism Matrix.toLin' it defines (Matrix.spectrum_toLin'), and the spectrum of an endomorphism of a finite-dimensional vector space with its eigenvalues (Module.End.hasEigenvalue_iff_mem_spectrum). This file records the composite in matrix language: a scalar lies in the spectrum of a matrix over a field exactly when the matrix has a nonzero eigenvector for it.

Main results

• Matrix.mem_spectrum_iff_exists_mulVec_eq_smul: μ ∈ spectrum K A if and only if A *ᵥ v = μ • v for some nonzero vector v.

theorem Matrix.mem_spectrum_iff_exists_mulVec_eq_smul {n : Type u_1} {K : Type u_2} [Fintype n] [DecidableEq n] [Field K] {A : Matrix n n K} {μ : K} : μ ∈ spectrum K A ↔ ∃ (v : n → K), v ≠ 0 ∧ A.mulVec v = μ • v

A scalar μ lies in the spectrum of a square matrix A over a field exactly when A has a nonzero eigenvector for μ.