proposition: Lemma map_lin1_mx m n (g : 'rV_m -> 'rV_n) gf : (forall v, (g v)^f = gf v^f) -> (lin1_mx g)^f = lin1_mx gf.
proof: Proof. move=> def_gf; apply/matrixP => i j; rewrite !mxE. by rewrite -(map_delta_mx f) -def_gf mxE. 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)