Documentation

Mathlib.LinearAlgebra.Eigenspace.Minpoly

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.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) :
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)
Equations
  • =