proposition: Lemma eigenpoly_map n (g : 'M_n) (p : {poly aF}) : eigenpoly (map_mx f g) (map_poly f p) = eigenpoly g p.
proof: Proof. by rewrite /eigenpoly -map_kermxpoly map_mx_eq0. 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)