proposition: Corollary prime_invariant_irr_extendible G N s p : N <| G -> #|G : N| = p -> prime p -> G \subset 'I['chi_s] -> {t | 'Res[N, G] 'chi_t = 'chi_s}.
proof: Proof. move=> nsNG iGN pr_p IGchi. have [t sGt] := constt_cfInd_irr s (normal_sub nsNG); exists t. have [e DtN]: exists e, 'Res 'chi_t = e%:R *: 'chi_s. rewrite constt_Ind_Res in sGt. rewrite (Clifford_Res_sum_cfclass nsNG sGt) cfclass_invariant // big_seq1. set e := '[_, _]; exists (Num.trunc e). by rewrite truncK ?Cnat_cfdot_char ?cfRes_char ?irr_char. have [/irrWnorm/eqP | [c injc DtNc]] := cfRes_prime_irr_cases t nsNG iGN pr_p. rewrite DtN cfnormZ cfnorm_irr normr_nat mulr1 -natrX pnatr_eq1. by rewrite muln_eq1 andbb => /eqP->; rewrite scale1r. have nz_e: e != 0. have: 'Res[N] 'chi_t != 0 by rewrite cfRes_eq0 // ?irr_char ?irr_neq0. by rewrite DtN; apply: contraNneq => ->; rewrite scale0r. have [i s'ci]: exists i, c i != s. pose i0 := Ordinal (prime_gt0 pr_p); pose i1 := Ordinal (prime_gt1 pr_p). have [<- | ] := eqVneq (c i0) s; last by exists i0. by exists i1; rewrite (inj_eq injc). have /esym/eqP/idPn[] := congr1 (cfdotr 'chi_(c i)) DtNc; rewrite {1}DtN /=. rewrite cfdot_suml cfdotZl cfdot_irr mulrb ifN_eqC // mulr0. rewrite (bigD1 i) //= cfnorm_irr big1 ?addr0 ?oner_eq0 // => j i'j. by rewrite cfdot_irr mulrb ifN_eq ?(inj_eq injc). 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)