proposition: Lemma map_mx_is_multiplicative n' (n := n'.+1) : multiplicative (map_mx f : 'M_n -> 'M_n).
proof: Proof. by split; [apply: map_mxM | apply: map_mx1]. 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)