proposition: Lemma signed_mx_repr rho : mx_repr 'SG_n (signed_mx rho).
proof: Proof. rewrite /signed_mx; split; first by rewrite /= odd_perm1 repr_mx1 expr0 scale1r. move=> g1 g2 _ _; rewrite odd_permM. by rewrite -scalemxAl -scalemxAr scalerA signr_addb repr_mxM ?inE. 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