proposition: Lemma irrEchar chi : (chi \in irr G) = (chi \is a character) && ('[chi] == 1).
proof: Proof. apply/irrP/andP=> [[i ->] | [Nchi]]; first by rewrite irr_char cfnorm_irr. rewrite cfdot_sum_irr => /eqP/natr_sum_eq1[i _| i [_ ci1 cj0]]. by rewrite rpredM // ?conj_natr ?Cnat_cfdot_char_irr. exists i; rewrite [chi]cfun_sum_cfdot (bigD1 i) //=. rewrite -(normr_idP (natr_ge0 (Cnat_cfdot_char_irr i Nchi))). rewrite normC_def {}ci1 sqrtC1 scale1r big1 ?addr0 // => j neq_ji. by rewrite (('[_] =P 0) _) ?scale0r // -normr_eq0 normC_def cj0 ?sqrtC0. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun eqtype choice ssrnat seq) mathcomp(path div fintype tuple finfun bigop prime order) mathcomp(ssralg poly finset gproduct fingroup morphism) mathcomp(perm automorphism quotient finalg action zmodp) mathcomp(commutator cyclic center pgroup nilpotent sylow) mathcomp(abelian matrix mxalgebra mxpoly mxrepresentation) mathcomp(vector ssrnum algC classfun archimedean)