proposition: Lemma degree_mxminpoly_map : degree_mxminpoly A^f = degree_mxminpoly A.
proof: Proof. by apply: eq_ex_minn => e; rewrite -map_powers_mx mxrank_map. 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)