proposition: Lemma triv_mx_repr : mx_repr 'SG_n triv_mx.
proof: Proof. by split => [//|g1 g2 _ _]; rewrite mul1mx. 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