Eigenvalues are the roots of the minimal polynomial.

Tags

eigenvalue, minimal polynomial

theorem Module.End.ker_aeval_ring_hom'_unit_polynomial {R : Type v} {M : Type w} [CommSemiring R] [AddCommMonoid M] [Module R M] (f : End R M) (c : (Polynomial R)ˣ) : LinearMap.ker ((Polynomial.aeval f) ↑c) = ⊥

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

theorem Module.End.isRoot_of_hasEigenvalue {R : Type v} {M : Type w} [CommRing R] [AddCommGroup M] [Module R M] [IsDomain R] [IsTorsionFree R M] {f : End R M} {μ : R} (h : f.HasEigenvalue μ) : (minpoly R f).IsRoot μ

theorem Module.End.hasEigenvalue_of_isRoot {R : Type v} {M : Type w} [CommRing R] [AddCommGroup M] [Module R M] {f : End R M} {μ : R} [IsDomain R] [Module.Finite R M] (h : (minpoly R f).IsRoot μ) : f.HasEigenvalue μ

theorem Module.End.hasEigenvalue_iff_isRoot {R : Type v} {M : Type w} [CommRing R] [AddCommGroup M] [Module R M] {f : End R M} {μ : R} [IsDomain R] [Module.Finite R M] [IsTorsionFree R M] : f.HasEigenvalue μ ↔ (minpoly R f).IsRoot μ

theorem Module.End.finite_hasEigenvalue {R : Type v} {M : Type w} [CommRing R] [AddCommGroup M] [Module R M] (f : End R M) [IsDomain R] [Module.Finite R M] [IsTorsionFree R M] : Set.Finite f.HasEigenvalue

@[implicit_reducible]

noncomputable instance Module.End.instFintypeEigenvalues {R : Type v} {M : Type w} [CommRing R] [AddCommGroup M] [Module R M] (f : End R M) [IsDomain R] [Module.Finite R M] [IsTorsionFree R M] : Fintype f.Eigenvalues

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

theorem Module.End.eigenspace_aeval_polynomial_degree_1 {K : Type v} {V : Type w} [Field K] [AddCommGroup V] [Module K V] (f : 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.finite_spectrum {K : Type v} {V : Type w} [Field K] [AddCommGroup V] [Module K V] [FiniteDimensional K V] (f : 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)