English
A rectangular-matrix version of the Cayley-Hamilton-type relation: X^card n * (A B).charpoly = X^card m * (B A).charpoly where A is m×n and B is n×m.
Русский
Версия для прямоугольных матриц: X^{|n|} (A B).charpoly = X^{|m|} (B A).charpoly, где A и B совместимы размера.
LaTeX
$$$X^{Fintype.card n} \cdot (A B).charpoly = X^{Fintype.card m} \cdot (B A).charpoly$$$
Lean4
/-- 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.
-/
theorem aeval_self_charpoly (M : Matrix n n R) : aeval M M.charpoly = 0 := by
-- We begin with the fact $χ_M(t) I = adjugate (t I - M) * (t I - M)$,
-- as an identity in `Matrix n n R[X]`.
have h : M.charpoly • (1 : Matrix n n R[X]) = adjugate (charmatrix M) * charmatrix M := (adjugate_mul _).symm
apply_fun matPolyEquiv at h
simp only [map_mul, matPolyEquiv_charmatrix] at h
apply_fun fun p => p.eval M at h
rw [eval_mul_X_sub_C] at h
rw [matPolyEquiv_smul_one, eval_map] at h
exact h
