Linear algebra · existing Mathlib theorem

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.

endomorphism
characteristic polynomial
polynomial evaluation
finite free module

Four separate status axes

Upstream indexedPinned source bytes verified locally

Locally reproducedExact upstream declaration replayed

Reviewed page2 of 3 presentation reviews recorded

Accepted Atlas resultNot recorded for the preferred artifact

These states distinguish upstream identity, local reproduction, review, and Atlas acceptance. This page is part of the public, read-only Mathlib landmark collection.

Formal orientation

Statement map

This deterministic map orients the reader from the mathematical summary to the pinned declaration and exact checked form. The HTML statement below is authoritative.

The theorem at a glance

Cayley–Hamilton theorem at a glance

A source-bound editorial overview of the exact Mathlib formulation. The image is explanatory; the statement map, formal type, and pinned source remain authoritative.

An ivory linear-algebra poster shows an unlabeled finite module lattice, cobalt endomorphism arcs, blank gold polynomial-combination layers, the formula chi sub f of f equals zero, and exact module scope. — A finite-free-module endomorphism satisfies its own characteristic polynomial.

A repeated sixteen-node module lattice passes through cobalt endomorphism arcs and gold polynomial layers before collapsing to sixteen calm empty positions. — The characteristic polynomial combines powers of the endomorphism into the zero map.

Complementary intuition

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.

The low-text schematic gives the theorem a visual identity; it does not replace the source-bound poster or exact statement.

Authoritative formal type

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

Selected evidence declaration text

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

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.

Proof Atlas did not originate the Cayley–Hamilton theorem or Mathlib's declaration.
The conclusion says that the characteristic polynomial evaluated at f is zero; it does not say that f itself is zero.
The generated explanation and visuals are not proof evidence.

Provenance

Origin and evidence stay separate

Existing declaration: LinearMap.aeval_self_charpoly in mathlib
Relationship: The checked artifact is the upstream declaration itself
Preferred checked artifact: artifact.library.mathlib.cayley-hamilton-theorem.v001
Source handling: Verified upstream reference; no mirrored source package