proposition: Lemma repr1_S0 (rho : reprS 0 1) : mx_rsim rho triv_repr.
proof: Proof. have /lin_char_irr/charSG0 cfrho := cfRepr1_lin_char rho. by apply: cfRepr_inj; rewrite cfrho cfRepr_triv. 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