proposition: Lemma sign_mx_repr : mx_repr 'SG_n sign_mx.
proof: Proof. rewrite /sign_mx; split; first by rewrite /= odd_perm1. by move=> g1 g2 _ _; rewrite odd_permM signr_addb. Qed.
imports: mathcomp(all_ssreflect) mathcomp(fingroup perm ssralg morphism perm action) mathcomp(zmodp) mathcomp(vector matrix mxalgebra ssrnum algC) mathcomp(mxrepresentation classfun character) permcomp tools partition congr cycles cycletype presentSn