proposition: Corollary cfRes_prime_irr_cases G N s p (chi := 'chi[G]_s) : N <| G -> #|G : N| = p -> prime p -> [\/ 'Res[N] chi \in irr N | exists2 c, injective c & 'Res[N] chi = \sum_(i < p) 'chi_(c i)].
proof: Proof. move=> /andP[sNG nNG] iGN pr_p. have chiefGN: chief_factor G N G. apply/andP; split=> //; apply/maxgroupP. split=> [|M /andP[/andP[sMG ltMG] _] sNM]. by rewrite /proper sNG -indexg_gt1 iGN prime_gt1. apply/esym/eqP; rewrite eqEsubset sNM -indexg_eq1 /= eq_sym. rewrite -(eqn_pmul2l (indexg_gt0 G M)) muln1 Lagrange_index // iGN. by apply/eqP/prime_nt_dvdP; rewrite ?indexg_eq1 // -iGN indexgS. have abGbar: abelian (G / N). by rewrite cyclic_abelian ?prime_cyclic ?card_quotient ?iGN. have IGchi: G \subset 'I[chi] by apply: sub_inertia. have [] := invariant_chief_irr_cases chiefGN abGbar IGchi; first by left. case=> e _ /(congr1 (fun m => odd (logn p m)))/eqP/idPn[]. by rewrite lognX mul2n odd_double iGN logn_prime // eqxx. by rewrite iGN; right. 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)