Eigenvalues are the roots of the minimal polynomial.

Tags

eigenvalue, minimal polynomial

theorem Module.End.eigenspace_aeval_polynomial_degree_1 {K : Type v} {V : Type w} [Field K] [AddCommGroup V] [Module K V] (f : Module.End K V) (q : Polynomial K) (hq : q.degree = 1) : f.eigenspace (-q.coeff 0 / q.leadingCoeff) = LinearMap.ker ((Polynomial.aeval f) q)

theorem Module.End.ker_aeval_ring_hom'_unit_polynomial {K : Type v} {V : Type w} [Field K] [AddCommGroup V] [Module K V] (f : Module.End K V) (c : (Polynomial K)ˣ) : LinearMap.ker ((Polynomial.aeval f) ↑c) = ⊥

theorem Module.End.aeval_apply_of_hasEigenvector {K : Type v} {V : Type w} [Field K] [AddCommGroup V] [Module K V] {f : Module.End K V} {p : Polynomial K} {μ : K} {x : V} (h : f.HasEigenvector μ x) : ((Polynomial.aeval f) p) x = Polynomial.eval μ p • x

theorem Module.End.isRoot_of_hasEigenvalue {K : Type v} {V : Type w} [Field K] [AddCommGroup V] [Module K V] {f : Module.End K V} {μ : K} (h : f.HasEigenvalue μ) : (minpoly K f).IsRoot μ

theorem Module.End.hasEigenvalue_of_isRoot {K : Type v} {V : Type w} [Field K] [AddCommGroup V] [Module K V] [FiniteDimensional K V] {f : Module.End K V} {μ : K} (h : (minpoly K f).IsRoot μ) : f.HasEigenvalue μ

theorem Module.End.hasEigenvalue_iff_isRoot {K : Type v} {V : Type w} [Field K] [AddCommGroup V] [Module K V] [FiniteDimensional K V] {f : Module.End K V} {μ : K} : f.HasEigenvalue μ ↔ (minpoly K f).IsRoot μ

theorem Module.End.finite_hasEigenvalue {K : Type v} {V : Type w} [Field K] [AddCommGroup V] [Module K V] [FiniteDimensional K V] (f : Module.End K V) : Set.Finite f.HasEigenvalue

noncomputable instance Module.End.instFintypeEigenvalues {K : Type v} {V : Type w} [Field K] [AddCommGroup V] [Module K V] [FiniteDimensional K V] (f : Module.End K V) : Fintype f.Eigenvalues

An endomorphism of a finite-dimensional vector space has finitely many eigenvalues.

Equations

• f.instFintypeEigenvalues = ⋯.fintype

theorem Module.End.finite_spectrum {K : Type v} {V : Type w} [Field K] [AddCommGroup V] [Module K V] [FiniteDimensional K V] (f : Module.End K V) : (spectrum K f).Finite

An endomorphism of a finite-dimensional vector space has a finite spectrum.

theorem Matrix.finite_spectrum {n : Type u_1} {R : Type u_2} [Field R] [Fintype n] [DecidableEq n] (A : Matrix n n R) : (spectrum R A).Finite

An n x n matrix over a field has a finite spectrum.

instance Matrix.instFiniteSpectrum {n : Type u_1} {R : Type u_2} [Field R] [Fintype n] [DecidableEq n] (A : Matrix n n R) : Finite ↑(spectrum R A)