proposition: Lemma repr1 n (rho : reprS n 1) : mx_rsim rho triv_repr \/ mx_rsim rho sign_repr.
proof: Proof. have /lin_char_Sn := cfRepr1_lin_char rho. by move=> [] cfrho; [left|right]; apply: cfRepr_inj; rewrite cfrho ?cfRepr_triv ?cfRepr_sign. 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