proposition: Lemma index_support_dvd_degree gT (G H : {group gT}) chi : H \subset G -> chi \is a character -> chi \in 'CF(G, H) -> (H :==: 1%g) || abelian G -> (#|G : H| %| chi 1%g)%C.
proof: Proof. move=> sHG Nchi Hchi ZHG. suffices: (#|G : H| %| 'Res[H] chi 1%g)%C by rewrite cfResE ?group1. rewrite ['Res _]cfun_sum_cfdot sum_cfunE rpred_sum // => i _. rewrite cfunE dvdC_mulr ?intr_nat ?Cnat_irr1 //. have [j ->]: exists j, 'chi_i = 'Res 'chi[G]_j. case/predU1P: ZHG => [-> | cGG] in i *. suffices ->: i = 0 by exists 0; rewrite !irr0 cfRes_cfun1 ?sub1G. apply/val_inj; case: i => [[|i] //=]; rewrite ltnNge NirrE. by rewrite (@leq_trans 1) // leqNgt classes_gt1 eqxx. have linG := char_abelianP G cGG; have linG1 j := eqP (proj2 (andP (linG j))). have /fin_all_exists[rH DrH] j: exists k, 'Res[H, G] 'chi_j = 'chi_k. apply/irrP/lin_char_irr/andP. by rewrite cfRes_char ?irr_char // cfRes1 ?linG1. suffices{i} all_rH: codom rH =i Iirr H. by exists (iinv (all_rH i)); rewrite DrH f_iinv. apply/subset_cardP; last exact/subsetP; apply/esym/eqP. rewrite card_Iirr_abelian ?(abelianS sHG) //. rewrite -(eqn_pmul2r (indexg_gt0 G H)) Lagrange //; apply/eqP. rewrite -sum_nat_const -card_Iirr_abelian // -sum1_card. rewrite (partition_big rH [in codom rH]) /=; last exact: image_f. have nsHG: H <| G by rewrite -sub_abelian_normal. apply: eq_bigr => _ /codomP[i ->]; rewrite -card_quotient ?normal_norm //. rewrite -card_Iirr_abelian ?quotient_abelian //. have Mlin j1 j2: exists k, 'chi_j1 * 'chi_j2 = 'chi[G]_k. exact/irrP/lin_char_irr/rpredM. have /fin_all_exists[rQ DrQ] (j : Iirr (G / H)) := Mlin i (mod_Iirr j). have mulJi: ('chi[G]_i)^*%CF * 'chi_i = 1. apply/cfun_inP=> x Gx; rewrite !cfunE /= -lin_charV_conj ?linG // cfun1E Gx. by rewrite lin_charV ?mulVf ?lin_char_neq0 ?linG. have inj_rQ: injective rQ. move=> j1 j2 /(congr1 (fun k => (('chi_i)^*%CF * 'chi_k) / H)%CF). by rewrite -!DrQ !mulrA mulJi !mul1r !mod_IirrE ?cfModK // => /irr_inj. rewrite -(card_imset _ inj_rQ) -sum1_card; apply: eq_bigl => j. rewrite -(inj_eq irr_inj) -!DrH; apply/eqP/imsetP=> [eq_ij | [k _ ->]]. have [k Dk] := Mlin (conjC_Iirr i) j; exists (quo_Iirr H k) => //. apply/irr_inj; rewrite -DrQ quo_IirrK //. by rewrite -Dk conjC_IirrE mulrCA mulrA mulJi mul1r. apply/subsetP=> x Hx; have Gx := subsetP sHG x Hx. rewrite cfkerEirr inE linG1 -Dk conjC_IirrE; apply/eqP. transitivity ((1 : 'CF(G)) x); last by rewrite cfun1E Gx. by rewrite -mulJi !cfunE -!(cfResE _ sHG Hx) eq_ij. rewrite -DrQ; apply/cfun_inP=> x Hx; rewrite !cfResE // cfunE mulrC. by rewrite cfker1 ?linG1 ?mul1r ?(subsetP _ x Hx) // mod_IirrE ?cfker_mod. have: (#|G : H| %| #|G : H|%:R * '[chi, 'chi_j])%C. by rewrite dvdC_mulr ?intr_nat ?Cnat_cfdot_char_irr. congr (_ %| _)%C; rewrite (cfdotEl _ Hchi) -(Lagrange sHG) mulnC natrM. rewrite invfM -mulrA mulVKf ?neq0CiG //; congr (_ * _). by apply: eq_bigr => x Hx; rewrite !cfResE. 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)