proposition: Lemma FTtypeP_ref_irr : {zeta | [/\ zeta \in irr M, zeta \in calS & zeta 1%g = w1%:R]}.
proof: Proof. have [_ /has_nonprincipal_irr[s nz_s] _ _ _] := Frobenius_context frobMbar. exists ('Ind 'chi_s %% M'')%CF; split. - by rewrite cfMod_irr ?irr_induced_Frobenius_ker ?(FrobeniusWker frobMbar). - by rewrite -cfIndMod ?normal_sub // -mod_IirrE // mem_calS mod_Iirr_eq0. rewrite -cfIndMod ?cfInd1 ?normal_sub // -(index_sdprod defM) cfMod1. by rewrite lin_char1 ?mulr1 //; apply/char_abelianP/sub_der1_abelian. Qed.
imports: mathcomp.ssreflect.ssreflect mathcomp(ssrbool ssrfun eqtype ssrnat seq path div choice fintype) mathcomp(tuple finfun bigop order prime ssralg poly finset center) mathcomp(fingroup morphism perm automorphism quotient action finalg zmodp) mathcomp(gfunctor gproduct cyclic commutator gseries nilpotent pgroup) mathcomp(sylow hall abelian maximal frobenius) mathcomp(matrix mxalgebra mxrepresentation mxabelem vector) odd_order(BGsection1 BGsection3 BGsection7 BGsection15 BGsection16) mathcomp(ssrnum algC classfun character integral_char inertia vcharacter) odd_order(PFsection1 PFsection2 PFsection3 PFsection4) odd_order(PFsection5 PFsection6 PFsection7 PFsection8 PFsection9)