proposition: Lemma triv_sign_not_sim n : (n > 1)%N -> ~ mx_rsim (G := [group of 'SG_n]) triv_repr sign_repr.
proof: Proof. move/triv_sign_neq => /negbTE Hneq /cfRepr_rsimP. by rewrite cfRepr_triv cfRepr_sign Hneq. 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