proposition: Theorem faithful_degree_p_part gT (p : nat) (G P : {group gT}) i : cfaithful 'chi[G]_i -> p.-nat (Num.trunc ('chi_i 1%g)) -> p.-Sylow(G) P -> abelian P -> 'chi_i 1%g = (#|G : 'Z(G)|`_p)%:R.
proof: Proof. have [p_pr | pr'p] := boolP (prime p); last first. have p'n n: (n > 0)%N -> p^'.-nat n. by move/p'natEpi->; rewrite mem_primes (negPf pr'p). rewrite irr1_degree natrK => _ /pnat_1-> => [_ _|]. by rewrite part_p'nat ?p'n. by rewrite p'n ?irr_degree_gt0. move=> fful_i /p_natP[a Dchi1] sylP cPP. have Dchi1C: 'chi_i 1%g = (p ^ a)%:R by rewrite -Dchi1 irr1_degree natrK. have pa_dv_ZiG: (p ^ a %| #|G : 'Z(G)|)%N. rewrite -dvdC_nat -[pa in (pa %| _)%C]Dchi1C -(cfcenter_fful_irr fful_i). exact: dvd_irr1_index_center. have [sPG pP p'PiG] := and3P sylP. have ZchiP: 'Res[P] 'chi_i \in 'CF(P, P :&: 'Z(G)). apply/cfun_onP=> x /[1!inE]; have [Px | /cfun0->//] := boolP (x \in P). rewrite /= -(cfcenter_fful_irr fful_i) cfResE //. apply: coprime_degree_support_cfcenter. rewrite Dchi1 coprimeXl // prime_coprime // -p'natE //. apply: pnat_dvd p'PiG; rewrite -index_cent1 indexgS // subsetI sPG. by rewrite sub_cent1 (subsetP cPP). have /andP[_ nZG] := center_normal G; have nZP := subset_trans sPG nZG. apply/eqP; rewrite Dchi1C eqr_nat eqn_dvd -{1}(pfactorK a p_pr) -p_part. rewrite partn_dvd //= -dvdC_nat -[pa in (_ %| pa)%C]Dchi1C -card_quotient //=. rewrite -(card_Hall (quotient_pHall nZP sylP)) card_quotient // -indexgI. rewrite -(cfResE _ sPG) // index_support_dvd_degree ?subsetIl ?cPP ?orbT //. by rewrite cfRes_char ?irr_char. 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)