proposition: Theorem primes_class_simple_gt1 C : simple G -> ~~ abelian G -> C \in (classes G)^# -> (size (primes #|C|) > 1)%N.
proof: Proof. move=> simpleG not_cGG /setD1P[ntC /imsetP[g Gg defC]]. have{ntC} nt_g: g != 1%g by rewrite defC classG_eq1 in ntC. rewrite ltnNge {C}defC; set m := #|_|; apply/negP=> p_natC. have{p_natC} [p p_pr [a Dm]]: {p : nat & prime p & {a | m = p ^ a}%N}. have /prod_prime_decomp->: (0 < m)%N by rewrite /m -index_cent1. rewrite prime_decompE; case Dpr: (primes _) p_natC => [|p []] // _. by exists 2%N => //; rewrite big_nil; exists 0. rewrite big_seq1; exists p; last by exists (logn p m). by have:= mem_primes p m; rewrite Dpr mem_head => /esym/and3P[]. have{simpleG} [ntG minG] := simpleP _ simpleG. pose p_dv1 i := (p %| 'chi[G]_i 1%g)%C. have p_dvd_supp_g i: ~~ p_dv1 i && (i != 0) -> 'chi_i g = 0. rewrite /p_dv1 irr1_degree dvdC_nat -prime_coprime // => /andP[co_p_i1 nz_i]. have fful_i: cfker 'chi_i = [1]. have /minG[//|/eqP] := cfker_normal 'chi_i. by rewrite eqEsubset subGcfker (negPf nz_i) andbF. have trivZ: 'Z(G) = [1] by have /minG[|/center_idP/idPn] := center_normal G. have trivZi: ('Z('chi_i))%CF = [1]. apply/trivgP; rewrite -quotient_sub1 ?norms1 //= -fful_i cfcenter_eq_center. rewrite fful_i subG1 -(isog_eq1 (isog_center (quotient1_isog G))) /=. by rewrite trivZ. rewrite coprime_degree_support_cfcenter ?trivZi ?inE //. by rewrite -/m Dm irr1_degree natrK coprime_sym coprimeXl. pose alpha := \sum_(i | p_dv1 i && (i != 0)) 'chi_i 1%g / p%:R * 'chi_i g. have nz_p: p%:R != 0 :> algC by rewrite pnatr_eq0 -lt0n prime_gt0. have Dalpha: alpha = - 1 / p%:R. apply/(canRL (mulfK nz_p))/eqP; rewrite -addr_eq0 addrC; apply/eqP/esym. transitivity (cfReg G g); first by rewrite cfRegE (negPf nt_g). rewrite cfReg_sum sum_cfunE (bigD1 0) //= irr0 !cfunE cfun11 cfun1E Gg. rewrite mulr1; congr (1 + _); rewrite (bigID p_dv1) /= addrC big_andbC. rewrite big1 => [|i /p_dvd_supp_g chig0]; last by rewrite cfunE chig0 mulr0. rewrite add0r big_andbC mulr_suml; apply: eq_bigr => i _. by rewrite mulrAC divfK // cfunE. suffices: (p %| 1)%C by rewrite (dvdC_nat p 1) dvdn1 -(subnKC (prime_gt1 p_pr)). rewrite unfold_in (negPf nz_p). rewrite Cint_rat_Aint ?rpred_div ?rpred1 ?rpred_nat //. rewrite -rpredN // -mulNr -Dalpha rpred_sum // => i /andP[/dvdCP[c Zc ->] _]. by rewrite mulfK // rpredM ?Aint_irr ?Aint_Cint. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq path) mathcomp(div choice fintype tuple finfun bigop prime order) mathcomp(ssralg poly finset fingroup morphism perm) mathcomp(automorphism quotient action countalg finalg zmodp) mathcomp(commutator cyclic center pgroup sylow gseries) mathcomp(nilpotent abelian ssrnum ssrint archimedean polydiv) mathcomp(rat matrix mxalgebra intdiv mxpoly vector falgebra) mathcomp(fieldext separable galois algC cyclotomic algnum) mathcomp(mxrepresentation classfun character)