proposition: Lemma odd_eq_conj_irr1 (G : {group gT}) t : odd #|G| -> (('chi[G]_t)^*%CF == 'chi_t) = ('chi_t == 1).
proof: Proof. rewrite -coprimen2 => oddG; pose A := <[1%R : 'Z_2]>. have Z2P (a : 'Z_2): a = 0 \/ a = 1 by apply/pred2P; case: a => -[|[]]. pose Ito (t : Iirr G) := [fun a : 'Z_2 => iter a (@conjC_Iirr _ G) t]. pose Cto (C : {set gT}) := [fun a : 'Z_2 => iter a invg C]. have IactP: is_action A Ito. split=> [|i /Z2P[]->] /Z2P[]-> //=; last by rewrite conjC_IirrK. exact/inv_inj/conjC_IirrK. have CactP: is_action A Cto. by split=> [|C /Z2P[]->] /Z2P[]-> //=; [apply: invg_inj | rewrite invgK]. pose Iact := Action IactP; pose Cact := Action CactP. have n_cG_A: [acts A, on classes G | Cact]. rewrite cycle_subG !inE cycle_id; apply/subsetP=> _ /imsetP[x Gx ->]. by rewrite !inE /= -classVg mem_classes ?groupV. transitivity (t \in [set 0]); last by rewrite inE irr_eq1. suffices{t} /eqP->: [set 0] == 'Fix_Iact[1]. by rewrite !inE sub1set inE -(inj_eq irr_inj) conjC_IirrE. rewrite eqEcard !(sub1set, inE) conjC_Iirr_eq0 eqxx /=. rewrite (card_afix_irr_classes (cycle_id _) n_cG_A) => [|i x xy Gx]; last first. rewrite inE => {xy}/imsetP[y Gy /(canRL invgK)->]. by rewrite -conjVg cfunJ {y Gy}//= conjC_IirrE cfunE/= -irr_inv invgK. have ->: #|[set 0 : Iirr G]| = #|[1 {set gT}]| by rewrite !cards1. apply/subset_leq_card/subsetP=> _ /setIdP[/imsetP[x Gx ->] /afix1P-DxGV]. have /imsetP[y Gy DxV]: x^-1%g \in x ^: G by rewrite -DxGV memV_invg class_refl. have{Gy} cxy: y \in 'C[x]. suffices cxy2: (y ^+ 2)%g \in 'C[x] by rewrite -(expgK oddG Gy) groupX. by rewrite cent1C cent1E conjgC conjgM -DxV conjVg -DxV invgK. rewrite inE classG_eq1 -in_set1 -(expgK oddG Gx) groupX // inE. by rewrite -eq_invg_mul DxV conjgE -(cent1P cxy) mulKg. Qed.
imports: mathcomp.ssreflect.ssreflect mathcomp(ssrbool ssrfun eqtype ssrnat seq path div choice fintype) mathcomp(tuple finfun bigop prime order ssralg finset fingroup morphism) mathcomp(perm automorphism quotient action zmodp finalg center commutator) mathcomp(poly cyclic pgroup nilpotent matrix mxalgebra mxrepresentation) mathcomp(vector falgebra fieldext ssrnum algC rat algnum galois) mathcomp(classfun character inertia integral_char vcharacter)