Documentation

Mathlib.LinearAlgebra.Eigenspace.Minpoly

Eigenvalues are the roots of the minimal polynomial. #

Tags #

eigenvalue, minimal polynomial

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) :
theorem Module.End.isRoot_of_hasEigenvalue {R : Type v} {M : Type w} [CommRing R] [AddCommGroup M] [Module R M] [NoZeroSMulDivisors 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 μ) :
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] [NoZeroSMulDivisors R M] :
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] [NoZeroSMulDivisors R M] :

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

Equations
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) :

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) :

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)