proposition: Lemma sign_char_subproof : is_class_fun <<'SG_n>> [ffun g => (-1) ^+ (odd_perm g)].
proof: Proof. rewrite genGid. by apply: intro_class_fun => /= [s t | s]; rewrite ?odd_permJ ?inE. 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