proposition: Corollary extend_solvable_coprime_irr G N t (theta := 'chi[N]_t) : N <| G -> solvable (G / N) -> G \subset 'I[theta] -> coprime #|G : N| ('o(theta)%CF * Num.trunc (theta 1%g)) -> exists c, [/\ 'Res 'chi[G]_c = theta, 'o('chi_c)%CF = 'o(theta)%CF & forall d, 'Res 'chi_d = theta -> coprime #|G : N| 'o('chi_d)%CF -> d = c].
proof: Proof. set e := #|G : N|; set f := Num.trunc _ => nsNG solG IGtheta. rewrite coprimeMr => /andP[co_e_th co_e_f]. have [sNG nNG] := andP nsNG; pose lambda := cfDet theta. have lin_lam: lambda \is a linear_char := cfDet_lin_char theta. have IGlam: G \subset 'I[lambda]. apply/subsetP=> y /(subsetP IGtheta)/setIdP[nNy /eqP th_y]. by rewrite inE nNy /= -cfDetConjg th_y. have co_e_lam: coprime e 'o(lambda)%CF by rewrite cfDet_order_lin. have [//|u [uNlam o_u Uu]] := extend_coprime_linear_char nsNG lin_lam IGlam. have /exists_eqP[c cNth]: [exists c, 'Res 'chi[G]_c == theta]. rewrite solvable_irr_extendible_from_det //. by apply/exists_eqP; exists u. have{c cNth} [c [cNth det_c] Uc] := extend_to_cfdet nsNG co_e_f cNth uNlam. have lin_u: 'chi_u \is a linear_char by rewrite -det_c cfDet_lin_char. exists c; split=> // [|c0 c0Nth co_e_c0]. by rewrite !cfDet_order_lin // -det_c in o_u. have lin_u0: cfDet 'chi_c0 \is a linear_char := cfDet_lin_char 'chi_c0. have /irrP[u0 Du0] := lin_char_irr lin_u0. have co_e_u0: coprime e 'o('chi_u0)%CF by rewrite -Du0 cfDet_order_lin. have eq_u0u: u0 = u by apply: Uu; rewrite // -Du0 -cfDetRes ?irr_char ?c0Nth. by apply: Uc; rewrite // Du0 eq_u0u. 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)