proposition: Lemma exists_linInd M : M \proper K -> M <| K -> exists2 phi, phi \in S M & phi 1%g = #|L : K|%:R.
proof: Proof. move=> ltMK nsMK; have [sMK nMK] := andP nsMK. have ntKM: (K / M)%g != 1%g by rewrite -subG1 quotient_sub1 // proper_subn. have [r lin_r ntr] := solvable_has_lin_char ntKM (quotient_sol M solK). pose i := mod_Iirr r; exists ('Ind[L] 'chi_i); last first. by rewrite cfInd1 ?mod_IirrE // cfMod1 lin_char1 ?mulr1. apply/seqIndP; exists i; rewrite // !inE subGcfker mod_IirrE ?cfker_mod //=. by rewrite mod_Iirr_eq0 // -irr_eq1 ntr. 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 zmodp) mathcomp(gfunctor gproduct cyclic pgroup commutator gseries nilpotent) mathcomp(sylow abelian maximal hall frobenius) mathcomp(matrix mxalgebra mxrepresentation vector ssrnum algC algnum) mathcomp(classfun character inertia vcharacter integral_char) odd_order(PFsection1 PFsection2 PFsection3 PFsection4 PFsection5)