proposition: Theorem Frobenius_Ind_irrP j : reflect (exists2 i, i != 0 & 'chi_j = 'Ind[G, K] 'chi_i) (~~ (K \subset cfker 'chi_j)).
proof: Proof. have [_ _ nsKG _] := Frobenius_kerP frobGK; have [sKG nKG] := andP nsKG. apply: (iffP idP) => [not_chijK1 | [i nzi ->]]; last first. by rewrite cfker_Ind_irr ?sub_gcore // subGcfker. have /neq0_has_constt[i chijKi]: 'Res[K] 'chi_j != 0 by apply: Res_irr_neq0. have nz_i: i != 0. by apply: contraNneq not_chijK1 => i0; rewrite constt0_Res_cfker // -i0. have /irrP[k def_chik] := irr_induced_Frobenius_ker nz_i. have: '['chi_j, 'chi_k] != 0 by rewrite -def_chik -cfdot_Res_l. by rewrite cfdot_irr pnatr_eq0; case: (j =P k) => // ->; exists i. 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)