proposition: Lemma map_cent_mx m n (E : 'A_(m, n)) : ('C(E)%MS)^f = 'C(E^f)%MS.
proof: Proof. rewrite map_kermx; congr kermx; apply: map_lin_mx => A; rewrite map_mxM. by congr (_ *m _); apply: map_lin_mx => B; rewrite map_mxB ?map_mxM. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq choice) mathcomp(fintype finfun bigop finset fingroup perm order) mathcomp(div prime binomial ssralg finalg zmodp matrix)