proposition: Lemma map_lin_mx m1 n1 m2 n2 (g : 'M_(m1, n1) -> 'M_(m2, n2)) gf : (forall A, (g A)^f = gf A^f) -> (lin_mx g)^f = lin_mx gf.
proof: Proof. move=> def_gf; apply: map_lin1_mx => A /=. by rewrite map_mxvec def_gf map_vec_mx. 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 countalg finalg zmodp)