proposition: Lemma lin_char_Sn n (xi : 'CF('SG_n)) : xi \is a linear_char -> xi = 1 \/ xi = sign_char.
proof: Proof. case: n xi => [|n] xi Hxi. by left; apply/cfunP => /= s; rewrite cfun1E inE /= permS0 lin_char1. have memSn p : p \in [set: 'S_n.+1]%G by rewrite in_setT. have ch1_eltr i : (i < n)%N -> xi 's_i = xi 's_0. move=> ltin; have [/= t ->] := eltr_conj (leq_ltn_trans (leq0n _) ltin) ltin. by rewrite /conjg lin_charM // mulrC -lin_charM // mulgK. have:= congr1 xi (eltr2 n 0); rewrite lin_charM // lin_char1 // => /eqP. rewrite -expr2 sqrf_eq1 => /orP[] /eqP xi_s0. - left; apply/cfunP => /= s; rewrite cfun1E inE /=. elim/eltr_ind: s => [|s i lti IHs]; first by rewrite lin_char1. by rewrite lin_charM // {}IHs mulr1 ch1_eltr. - right; apply/cfunP => /= s; rewrite cfunE. elim/eltr_ind: s => [|s i lti IHs]. by rewrite lin_char1 // odd_perm1 expr0. rewrite lin_charM // {}IHs odd_permM odd_eltr // ch1_eltr // xi_s0. by rewrite mulN1r // signrN. 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