proposition: Theorem dvd_irr1_cardG gT (G : {group gT}) i : ('chi[G]_i 1%g %| #|G|)%C.
proof: Proof. rewrite unfold_in -if_neg irr1_neq0 Cint_rat_Aint //=. by rewrite rpred_div ?rpred_nat // rpred_nat_num ?Cnat_irr1. rewrite -[n in n / _]/(_ *+ true) -(eqxx i) -mulr_natr. rewrite -first_orthogonality_relation mulVKf ?neq0CG //. rewrite sum_by_classes => [|x y Gx Gy]; rewrite -?conjVg ?cfunJ //. rewrite mulr_suml rpred_sum // => K /repr_classesP[Gx {1}->]. by rewrite !mulrA mulrAC rpredM ?Aint_irr ?Aint_class_div_irr1. 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)