proposition: Lemma cfBigdprod_eq1 phi : (forall i, P i -> phi i \is a character) -> (cfBigdprod defG phi == 1) = [forall (i | P i), phi i == 1].
proof: Proof. move=> Nphi; set Phi := cfBigdprod defG phi. apply/eqP/eqfun_inP=> [Phi1 i Pi | phi1]; last first. by apply: big1 => i /phi1->; rewrite rmorph1. have Phi1_1: Phi 1%g = 1 by rewrite Phi1 cfun1E group1. have nz_Phi1: Phi 1%g != 0 by rewrite Phi1_1 oner_eq0. have [_ <-] := cfBigdprodK nz_Phi1 Pi. rewrite Phi1_1 divr1 -/Phi Phi1 rmorph1. rewrite prod_cfunE // in Phi1_1; have := natr_prod_eq1 _ Phi1_1 Pi. rewrite -(cfRes1 (A i)) cfBigdprodiK // => ->; first by rewrite scale1r. by move=> {i Pi} j /Nphi Nphi_j; rewrite Cnat_char1 ?cfBigdprodi_char. 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)