proposition: Lemma irr1_abelian_bound (i : Iirr G) : abelian (G / 'Z('chi_i)%CF) -> ('chi_i 1%g) ^+ 2 = #|G : 'Z('chi_i)%CF|%:R.
proof: Proof. move=> AbGc; apply/eqP; rewrite irr1_bound cfun_onE; apply/subsetP=> x nz_chi_x. have Gx: x \in G by apply: contraR nz_chi_x => /cfun0->. have nKx := subsetP (normal_norm (cfker_normal 'chi_i)) _ Gx. rewrite -(quotientGK (cfker_center_normal _)) inE nKx inE /=. rewrite cfcenter_eq_center inE mem_quotient //=. apply/centP=> _ /morphimP[y nKy Gy ->]; apply/commgP; rewrite -morphR //=. set z := [~ x, y]; rewrite coset_id //. have: z \in 'Z('chi_i)%CF. apply: subsetP (mem_commg Gx Gy). by rewrite der1_min // normal_norm ?cfcenter_normal. rewrite -irrRepr cfker_repr cfcenter_repr !inE in nz_chi_x *. case/andP=> Gz /is_scalar_mxP[c Chi_z]; rewrite Gz Chi_z mul1mx /=. apply/eqP; congr _%:M; apply: (mulIf nz_chi_x); rewrite mul1r. rewrite -{2}(cfunJ _ x Gy) conjg_mulR -/z !cfunE Gx groupM // !{1}mulrb. by rewrite repr_mxM // Chi_z mul_mx_scalar mxtraceZ. 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)