Mathlib theorem · Existing formal mathematics
ProofAtlas

Existing in Mathlib · Linear algebra

Cayley–Hamilton Theorem

Take a linear transformation of a finite free module, form its characteristic polynomial, and substitute the transformation itself into that polynomial. The resulting endomorphism is zero.

Exact theorem

Exact Mathlib statement

theorem LinearMap.aeval_self_charpoly {R : Type*} {M : Type*} [CommRing R] [AddCommGroup M] [Module R M] [Module.Free R M] [Module.Finite R M] (f : M →ₗ[R] M) : (Polynomial.aeval f) f.charpoly = 0

The theorem at a glance

Cayley–Hamilton theorem at a glance

A visual guide to the theorem's hypotheses, structure, and conclusion; the exact statement gives the formal detail.

A finite-free-module endomorphism satisfies its own characteristic polynomial. Explanatory diagram.
Detailed visual description

The poster distinguishes an endomorphism from the zero polynomial evaluation, shows the matrix-mediated transformation route without field-only language, and states the commutative-ring finite-free-module scope.

Statement structure

Statement and scope

Statement map for Cayley–Hamilton TheoremAn endomorphism of a finite free module over a commutative ring annihilates its own characteristic polynomial. Claim boundary: This target indexes Mathlib's theorem that a linear endomorphism of a finite free module over a commutative ring annihilates its own characteristic polynomial. It is not restricted to matrices over a field and does not claim a new proof. The pinned upstream declaration is LinearMap.aeval_self_charpoly. The complete formal statement is available in the Exact Mathlib statement section.Mathematical readingAn endomorphism of afinite free module overa commutative ringannihilates its owncharacteristicpolynomial.Claim boundaryThis target indexesMathlib's theorem that alinear endomorphism of afinite free module overa commutative ringannihilates its owncharacteristicpolynomial. It is notrestricted to matricesover a field and doesnot claim a new proof.Pinned declarationmathlib ·LinearMap.aeval_self_charpolyStatement map for Cayley–Hamilton TheoremAn endomorphism of a finite free module over a commutative ring annihilates its own characteristic polynomial. Claim boundary: This target indexes Mathlib's theorem that a linear endomorphism of a finite free module over a commutative ring annihilates its own characteristic polynomial. It is not restricted to matrices over a field and does not claim a new proof. The pinned upstream declaration is LinearMap.aeval_self_charpoly. The complete formal statement is available in the Exact Mathlib statement section.Mathematical readingAn endomorphism of afinite free module overa commutative ringannihilates its owncharacteristicpolynomial.Claim boundaryThis target indexesMathlib's theorem that alinear endomorphism of afinite free module overa commutative ringannihilates its owncharacteristicpolynomial. It is notrestricted to matricesover a field and doesnot claim a new proof.Pinned declarationmathlib ·LinearMap.aeval_self_charpoly

Read the exact Mathlib declaration

This map summarizes the statement's structure; the exact Mathlib declaration remains authoritative.

Evaluating f's characteristic polynomial at f gives the zero endomorphism. Explanatory scientific diagram.
Detailed visual description

The lattice M with loop arrow f leads to a blue box χ_f(T), a substitution arrow T ↦ f, and a green box χ_f(f) = 0_End(M). Below, vectors v₁, v₂, …, vₖ pass through the same polynomial-evaluation box and reach zero. This illustrates an endomorphism of a finite free module over a commutative ring. The zero belongs to the whole polynomial evaluation, not to f.

Why it matters

A mathematical landmark

Cayley–Hamilton binds the polynomial invariants of a linear transformation back to the transformation itself. It is a cornerstone of matrix theory and module-theoretic linear algebra.

ProofAtlas record

What has been checked

Upstream indexedPinned source bytes verified locally
Locally reproducedExact upstream declaration replayed
Reviewed pageCurrent public presentation reviewed
Accepted Atlas resultNot recorded for the preferred artifact

Mathlib is the source of the theorem; the local Lean replay and page review are separate.

Claim boundary

No new theorem is claimed

This target indexes Mathlib's theorem that a linear endomorphism of a finite free module over a commutative ring annihilates its own characteristic polynomial. It is not restricted to matrices over a field and does not claim a new proof.

Source and local evidence

Where the theorem comes from

Existing declaration
LinearMap.aeval_self_charpoly in mathlib
Relationship
The checked artifact is the upstream declaration itself
Local Lean evidence
artifact.library.mathlib.cayley-hamilton-theorem.v001
Source
Open the pinned upstream reference