Theorems · Theorem · linear algebra

Matrix.aeval_self_charpoly

• #49 of the 100 theorems: The Cayley-Hamilton Theorem
• 1000+ list: Cayley–Hamilton theorem

∀ {R : Type u_1} [inst : CommRing R] {n : Type u_4} [inst_1 : DecidableEq n] [inst_2 : Fintype n] (M : Matrix n n R),
  (Polynomial.aeval M) M.charpoly = 0

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.

Defined in

Mathlib.LinearAlgebra.Matrix.Charpoly.Basic

Cited by

6 results in Mathlib

Foundations

Depth 125 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

CommRingDecidableEqFintype