proposition: Lemma mxminpoly_map : mxminpoly A^f = fp (mxminpoly A).
proof: Proof. rewrite rmorphB; congr (_ - _). by rewrite /= map_polyXn degree_mxminpoly_map. rewrite degree_mxminpoly_map -rmorphXn /=. apply/polyP=> i; rewrite coef_map //= !coef_rVpoly degree_mxminpoly_map. case/insub: i => [i|]; last by rewrite rmorph0. by rewrite -map_powers_mx -map_pinvmx // -map_mxvec -map_mxM // mxE. 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)