# Documentation

Mathlib.LinearAlgebra.Eigenspace.Basic

# Eigenvectors and eigenvalues #

This file defines eigenspaces, eigenvalues, and eigenvalues, as well as their generalized counterparts. We follow Axler's approach [axler2015] because it allows us to derive many properties without choosing a basis and without using matrices.

An eigenspace of a linear map f for a scalar μ is the kernel of the map (f - μ • id). The nonzero elements of an eigenspace are eigenvectors x. They have the property f x = μ • x. If there are eigenvectors for a scalar μ, the scalar μ is called an eigenvalue.

There is no consensus in the literature whether 0 is an eigenvector. Our definition of HasEigenvector permits only nonzero vectors. For an eigenvector x that may also be 0, we write x ∈ f.eigenspace μ.

A generalized eigenspace of a linear map f for a natural number k and a scalar μ is the kernel of the map (f - μ • id) ^ k. The nonzero elements of a generalized eigenspace are generalized eigenvectors x. If there are generalized eigenvectors for a natural number k and a scalar μ, the scalar μ is called a generalized eigenvalue.

The fact that the eigenvalues are the roots of the minimal polynomial is proved in LinearAlgebra.Eigenspace.Minpoly.

The existence of eigenvalues over an algebraically closed field (and the fact that the generalized eigenspaces then span) is deferred to LinearAlgebra.Eigenspace.IsAlgClosed.

• [Sheldon Axler, Linear Algebra Done Right][axler2015]
• https://en.wikipedia.org/wiki/Eigenvalues_and_eigenvectors

## Tags #

eigenspace, eigenvector, eigenvalue, eigen