proposition: Theorem dvd_irr1_index_center gT (G : {group gT}) i : ('chi[G]_i 1%g %| #|G : 'Z('chi_i)%CF|)%C.
proof: Proof. without loss fful: gT G i / cfaithful 'chi_i. rewrite -{2}[i](quo_IirrK _ (subxx _)) 1?mod_IirrE ?cfModE ?cfker_normal //. rewrite morph1; set i1 := quo_Iirr _ i => /(_ _ _ i1) IH. have fful_i1: cfaithful 'chi_i1. by rewrite quo_IirrE ?cfker_normal ?cfaithful_quo. have:= IH fful_i1; rewrite cfcenter_fful_irr // -cfcenter_eq_center. rewrite index_quotient_eq ?cfcenter_sub ?cfker_norm //. by rewrite setIC subIset // normal_sub ?cfker_center_normal. have [lambda lin_lambda Dlambda] := cfcenter_Res 'chi_i. have DchiZ: {in G & 'Z(G), forall x y, 'chi_i (x * y)%g = 'chi_i x * lambda y}. rewrite -(cfcenter_fful_irr fful) => x y Gx Zy. apply: (mulfI (irr1_neq0 i)); rewrite mulrCA. transitivity ('chi_i x * ('chi_i 1%g *: lambda) y); last by rewrite !cfunE. rewrite -Dlambda cfResE ?cfcenter_sub //. rewrite -irrRepr cfcenter_repr !cfunE in Zy *. case/setIdP: Zy => Gy /is_scalar_mxP[e De]. rewrite repr_mx1 group1 (groupM Gx Gy) (repr_mxM _ Gx Gy) Gx Gy De. by rewrite mul_mx_scalar mxtraceZ mulrCA mulrA mulrC -mxtraceZ scalemx1. have inj_lambda: {in 'Z(G) &, injective lambda}. rewrite -(cfcenter_fful_irr fful) => x y Zx Zy eq_xy. apply/eqP; rewrite eq_mulVg1 -in_set1 (subsetP fful) // cfkerEirr inE. apply/eqP; transitivity ('Res['Z('chi_i)%CF] 'chi_i (x^-1 * y)%g). by rewrite cfResE ?cfcenter_sub // groupM ?groupV. rewrite Dlambda !cfunE lin_charM ?groupV // -eq_xy -lin_charM ?groupV //. by rewrite mulrC mulVg lin_char1 ?mul1r. rewrite unfold_in -if_neg irr1_neq0 Cint_rat_Aint //. by rewrite rpred_div ?rpred_nat // rpred_nat_num ?Cnat_irr1. rewrite (cfcenter_fful_irr fful) nCdivE natf_indexg ?center_sub //=. have ->: #|G|%:R = \sum_(x in G) 'chi_i x * 'chi_i (x^-1)%g. rewrite -[_%:R]mulr1; apply: canLR (mulVKf (neq0CG G)) _. by rewrite first_orthogonality_relation eqxx. rewrite (big_setID [set x | 'chi_i x == 0]) /= -setIdE. rewrite big1 ?add0r => [| x /setIdP[_ /eqP->]]; last by rewrite mul0r. pose h x := (x ^: G * 'Z(G))%g; rewrite (partition_big_imset h). rewrite !mulr_suml rpred_sum //= => _ /imsetP[x /setDP[Gx nz_chi_x] ->]. have: #|x ^: G|%:R * ('chi_i x * 'chi_i x^-1%g) / 'chi_i 1%g \in Aint. by rewrite !mulrA mulrAC rpredM ?Aint_irr ?Aint_class_div_irr1. congr 2 (_ * _ \in Aint); apply: canRL (mulfK (neq0CG _)) _. rewrite inE in nz_chi_x. transitivity ('chi_i x * 'chi_i (x^-1)%g *+ #|h x|); last first. rewrite -sumr_const. apply: eq_big => [y | _ /mulsgP[_ z /imsetP[u Gu ->] Zz] ->]. rewrite !inE -andbA; apply/idP/and3P=> [|[_ _ /eqP <-]]; last first. by rewrite -{1}[y]mulg1 mem_mulg ?class_refl. case/mulsgP=> _ z /imsetP[u Gu ->] Zz ->; have /centerP[Gz cGz] := Zz. rewrite groupM 1?DchiZ ?groupJ ?cfunJ //; split=> //. by rewrite mulf_neq0 // lin_char_neq0 /= ?cfcenter_fful_irr. rewrite -[z](mulKg u) -cGz // -conjMg /h classGidl {u Gu}//. apply/eqP/setP=> w; apply/mulsgP/mulsgP=> [][_ z1 /imsetP[v Gv ->] Zz1 ->]. exists (x ^ v)%g (z * z1)%g; rewrite ?imset_f ?groupM //. by rewrite conjMg -mulgA /(z ^ v)%g cGz // mulKg. exists ((x * z) ^ v)%g (z^-1 * z1)%g; rewrite ?imset_f ?groupM ?groupV //. by rewrite conjMg -mulgA /(z ^ v)%g cGz // mulKg mulKVg. rewrite !irr_inv DchiZ ?groupJ ?cfunJ // rmorphM mulrACA -!normCK -exprMn. by rewrite (normC_lin_char lin_lambda) ?mulr1 //= cfcenter_fful_irr. rewrite mulrAC -natrM mulr_natl; congr (_ *+ _). symmetry; rewrite /h /mulg /= /set_mulg [in _ @2: (_, _)]unlock cardsE. rewrite -cardX card_in_image // => [] [y1 z1] [y2 z2] /=. move=> /andP[/=/imsetP[u1 Gu1 ->] Zz1] /andP[/=/imsetP[u2 Gu2 ->] Zz2] {y1 y2}. move=> eq12; have /eqP := congr1 'chi_i eq12. rewrite !(cfunJ, DchiZ) ?groupJ // (can_eq (mulKf nz_chi_x)). rewrite (inj_in_eq inj_lambda) // => /eqP eq_z12; rewrite eq_z12 in eq12 *. by rewrite (mulIg _ _ _ eq12). 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)