Endomorphism polynomials

DefinitionMinimal polynomial#

Suppose x : B, where B is an A-algebra.

The minimal polynomial minpoly A x of x is a monic polynomial with coefficients in A of smallest degree that has x as its root, if such exists (IsIntegral A x) or zero otherwise.

For example, if V is a 𝕜-vector space for some field 𝕜 and f : V →ₗ[𝕜] V then the minimal polynomial of f is minpoly 𝕜 f.

minpoly.{u_1, u_2} (A : Type u_1) {B : Type u_2} [CommRing A] [Ring B] [Algebra A B] (x : B) :
  Polynomial A
Sources
Mathlibminpoly
Uses 2 · Used by 6
Statement usesAssociative algebra over a commutative ring · Polynomial in one indeterminate
Used byDirichlet unit theorem · Abel-Ruffini theorem (one direction) · Existence of algebraic closure of a field · Galois correspondence · Primitive element theorem · Jordan-Chevalley-Dunford decomposition

DefinitionCharacteristic polynomial#

The characteristic polynomial of a matrix M is given by \(\det (t I - M)\).

Matrix.charpoly.{u_1, u_4} {R : Type u_1} [CommRing R] {n : Type u_4} [DecidableEq n] [Fintype n]
  (M : Matrix n n R) : Polynomial R
Sources
MathlibMatrix.charpoly
Uses 2 · Used by 1
Statement usesDeterminant · Polynomial in one indeterminate
Used byCayley-Hamilton theorem

TheoremCayley-Hamilton theorem#

The Cayley-Hamilton Theorem, that the characteristic polynomial of a matrix, applied to the matrix itself, is zero.

This holds over any commutative ring.

See LinearMap.aeval_self_charpoly for the equivalent statement about endomorphisms.

Matrix.aeval_self_charpoly.{u_1, u_4} {R : Type u_1} [CommRing R] {n : Type u_4} [DecidableEq n]
  [Fintype n] (M : Matrix n n R) : (Polynomial.aeval M) M.charpoly = 0
Sources
MathlibMatrix.aeval_self_charpoly
Uses 4
Statement usesCharacteristic polynomial
Proof usesAlgebra of endomorphisms of a vector space · Polynomial functions · Tensor product of algebras

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.