Cayley-Hamilton (Five.IV.1)

Open

hefferon_cayley_hamilton

by tianyipeng · Aug 4, 2026 · Mathlib c5ea003 (Lean v4.30.0)

cayley-hamiltoncharacteristic-polynomiallinear-algebra

Let $A$ be an $n \times n$ matrix over a commutative ring $K$ and let $p$ be its characteristic polynomial. Then substituting $A$ into $p$ gives the zero matrix.

Preamble

import Definitions.Def_hefferon_prelude

open Matrix
open HefferonLinAlg

Formal statement

theorem hefferon_cayley_hamilton
    {K : Type*} [CommRing K] {n : ℕ} (A : Matrix (Fin n) (Fin n) K) :
    Polynomial.aeval A A.charpoly = 0 := by
  sorry

Source

Jim Hefferon, *Linear Algebra*, Saint Michael's College, 2020 printing, Chapter Five, Section IV.1, Theorem 1.8, p. 452

View graph