proposition: Theorem Cayley_Hamilton (R : comRingType) n' (A : 'M[R]_n'.+1) : horner_mx A (char_poly A) = 0.
proof: Proof. have [phi [_ phiZ phiC _]] := mx_poly_ring_isom R n'. apply/rootP/factor_theorem; rewrite -phiZ -mul_adj_mx rmorphM /=. by move: (phi _) => q; exists q; rewrite rmorphB phiC phiZ map_polyX. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat choice seq) mathcomp(div fintype tuple finfun bigop fingroup perm) mathcomp(ssralg zmodp matrix mxalgebra poly polydiv)