proposition: Lemma sign_char2 : sign_char = 'chi_(cast_ord (esym NirrS2) 1).
proof: Proof. Proof using. have /irrP[j Hj] := lin_char_irr (@sign_charP 2). rewrite -(cast_IirrS2 (i := j)) //; apply/eqP => Hj0; subst j. by have := triv_sign_neq (n := 2) (ltnSn _); rewrite Hj irr0 eqxx. 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