Cayley–Hamilton for an endomorphism represented by a matrix #
Let b : ι → M span the R-module M. If a square matrix A represents the endomorphism f
on b (Matrix.Represents), then f is a root of the characteristic polynomial of A. This is
the step from the matrix Cayley–Hamilton theorem Matrix.aeval_self_charpoly to endomorphisms of
finitely generated modules that Mathlib performs inside the proof of
LinearMap.exists_monic_and_natDegree_eq_and_coeff_mem_pow_and_aeval_eq_zero, stated for a
given representing matrix, so that the polynomial can be read off from the matrix.
Main results #
Matrix.Represents.aeval_charpoly_eq_zero: ifArepresentsfon a spanning family, thenaeval f A.charpoly = 0.
theorem
Matrix.Represents.aeval_charpoly_eq_zero
{ι : Type u_1}
[Fintype ι]
[DecidableEq ι]
{R : Type u_2}
{M : Type u_3}
[CommRing R]
[AddCommGroup M]
[Module R M]
{b : ι → M}
(hb : Submodule.span R (Set.range b) = ⊤)
{A : Matrix ι ι R}
{f : Module.End R M}
(h : Represents b A f)
:
Cayley–Hamilton along a representation. If A represents the endomorphism f on a family
b spanning M, then f is a root of the characteristic polynomial of A.