proposition: Lemma dvdn_constt_Res1_irr1 i j : H <| G -> j \in irr_constt ('Res[H, G] 'chi_i) -> exists n, 'chi_i 1%g = n%:R * 'chi_j 1%g.
proof: Proof. move=> nsHG chiHj; have [sHG nHG] := andP nsHG; rewrite -(cfResE _ sHG) //. rewrite {1}(Clifford_Res_sum_cfclass nsHG chiHj) cfunE sum_cfunE. have /natrP[n ->]: '['Res[H] 'chi_i, 'chi_j] \in Num.nat. by rewrite Cnat_cfdot_char ?cfRes_char ?irr_char. exists (n * size ('chi_j ^: G)%CF)%N; rewrite natrM -mulrA; congr (_ * _). rewrite mulr_natl -[size _]card_ord big_tnth -sumr_const; apply: eq_bigr => k _. by have /cfclassP[y Gy ->]:= mem_tnth k (in_tuple _); rewrite cfConjg1. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq path) mathcomp(choice fintype div tuple finfun bigop prime order) mathcomp(ssralg ssrnum finset fingroup morphism perm) mathcomp(automorphism quotient action zmodp cyclic center) mathcomp(gproduct commutator gseries nilpotent pgroup) mathcomp(sylow maximal frobenius matrix mxalgebra) mathcomp(mxrepresentation vector algC classfun character) mathcomp(archimedean)