proposition: Lemma repr_S2 (rho : representation algC [group of 'SG_2]) : mx_irreducible rho -> mx_rsim rho triv_repr \/ mx_rsim rho sign_repr.
proof: Proof. Proof using. move=> Hirr. have : cfRepr rho \in irr 'SG_2 by apply/irr_reprP; exists rho. rewrite irr_S2 memtE tval_tcastE !inE. by move=> /orP[]/eqP cfRho; [left | right]; apply: cfRepr_inj; rewrite ?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