Structure theory of endomorphisms

AbbreviationEigenvalue#

A scalar μ is an eigenvalue for a linear map f if there are nonzero vectors x such that f x = μ • x. (Def 5.5 of axler2024).

Module.End.HasEigenvalue.{v, w} {R : Type v} {M : Type w} [CommRing R] [AddCommGroup M]
  [_root_.Module R M] (f : Module.End R M) (a : R) : Prop
Sources
MathlibModule.End.HasEigenvalue
Uses 1 · Used by 4
Statement usesGeneralized eigenspaces
Used byDiagonalization of self-adjoint endomorphisms · Existence of an eigenvalue · Gershgorin circle theorem · Lie's theorem

AbbreviationEigenvector#

A nonzero element of an eigenspace is an eigenvector. (Def 5.8 of axler2024)

Module.End.HasEigenvector.{v, w} {R : Type v} {M : Type w} [CommRing R] [AddCommGroup M]
  [_root_.Module R M] (f : Module.End R M) (μ : R) (x : M) : Prop
Sources
MathlibModule.End.HasEigenvector
Uses 1 · Used by 3
Statement usesGeneralized eigenspaces
Used byEigenvalues from Rayleigh quotient · Gershgorin circle theorem · Lie's theorem

TheoremExistence of an eigenvalue#

In finite dimensions, over an algebraically closed field, every linear endomorphism has an eigenvalue.

Module.End.exists_eigenvalue.{u_1, u_2} {K : Type u_1} {V : Type u_2} [Field K] [AddCommGroup V]
  [_root_.Module K V] [IsAlgClosed K] [FiniteDimensional K V] [Nontrivial V] (f : Module.End K V) :
  ∃ c, f.HasEigenvalue c
Sources
MathlibModule.End.exists_eigenvalue
Uses 5
Statement usesAlgebraically closed field · Eigenvalue · Finite-dimensionality
Proof usesAlgebra of endomorphisms of a vector space · Basis

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.