proposition: Lemma irr_S2 : irr 'SG_2 = tcast (esym NirrS2) [tuple 1; sign_char].
proof: Proof. Proof using. apply eq_from_tnth => i; case: (i =P 0) => [-> | /eqP Hi]. - by rewrite tcastE irr0. - by rewrite tcastE sign_char2 (cast_IirrS2 Hi). 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