proposition: Lemma eigenspace_poly n a (f : 'M_n) : eigenspace f a = kermxpoly f ('X - a%:P).
proof: Proof. case: n => [|m] in a f *; first by rewrite !thinmx0. by congr (kermx _); rewrite rmorphB /= ?horner_mx_X ?horner_mx_C. 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)