proposition: Corollary extend_coprime_linear_char G N (lambda : 'CF(N)) : N <| G -> lambda \is a linear_char -> G \subset 'I[lambda] -> coprime #|G : N| 'o(lambda)%CF -> exists u, [/\ 'Res 'chi[G]_u = lambda, 'o('chi_u)%CF = 'o(lambda)%CF & forall v, 'Res 'chi_v = lambda -> coprime #|G : N| 'o('chi_v)%CF -> v = u].
proof: Proof. set e := #|G : N| => nsNG lam_lin IGlam co_e_lam; have [sNG nNG] := andP nsNG. have [p lam_p | v vNlam] := extend_linear_char_from_Sylow nsNG lam_lin IGlam. exists N; last first. by have /irrP[u ->] := lin_char_irr lam_lin; exists u; rewrite cfRes_id. split=> //; rewrite trivg_quotient /pHall sub1G pgroup1 indexg1. rewrite card_quotient //= -/e (pi'_p'nat _ lam_p) //. rewrite -coprime_pi' ?indexg_gt0 1?coprime_sym //. by have:= lam_p; rewrite mem_primes => /and3P[]. set nu := 'chi_v in vNlam. have lin_nu: nu \is a linear_char. by rewrite (@cfRes_lin_lin _ _ N) ?vNlam ?irr_char. have [b be_mod_lam]: exists b, b * e = 1 %[mod 'o(lambda)%CF]. rewrite -(chinese_modr co_e_lam 0 1) /chinese !mul0n !mul1n mulnC. by set b := _.1; exists b. have /irrP[u Du]: nu ^+ (b * e) \in irr G by rewrite lin_char_irr ?rpredX. exists u; set mu := 'chi_u in Du *. have uNlam: 'Res mu = lambda. rewrite cfDet_order_lin // in be_mod_lam. rewrite -Du rmorphXn /= vNlam -(expr_mod _ (exp_cforder _)) //. by rewrite be_mod_lam expr_mod ?exp_cforder. have lin_mu: mu \is a linear_char by rewrite -Du rpredX. have o_mu: ('o(mu) = 'o(lambda))%CF. have dv_o_lam_mu: 'o(lambda)%CF %| 'o(mu)%CF. by rewrite !cfDet_order_lin // -uNlam cforder_Res. have kerNnu_olam: N \subset cfker (nu ^+ 'o(lambda)%CF). rewrite -subsetIidl -cfker_Res ?rpredX ?irr_char //. by rewrite rmorphXn /= vNlam cfDet_order_lin // exp_cforder cfker_cfun1. apply/eqP; rewrite eqn_dvd dv_o_lam_mu andbT cfDet_order_lin //. rewrite dvdn_cforder -Du exprAC -dvdn_cforder dvdn_mull //. rewrite -(cfQuoK nsNG kerNnu_olam) cforder_mod // /e -card_quotient //. by rewrite cforder_lin_char_dvdG ?cfQuo_lin_char ?rpredX. split=> // t tNlam co_e_t. have lin_t: 'chi_t \is a linear_char. by rewrite (@cfRes_lin_lin _ _ N) ?tNlam ?irr_char. have Ut := lin_char_unitr lin_t. have kerN_mu_t: N \subset cfker (mu / 'chi_t)%R. rewrite -subsetIidl -cfker_Res ?lin_charW ?rpred_div ?rmorph_div //. by rewrite /= uNlam tNlam divrr ?lin_char_unitr ?cfker_cfun1. have co_e_mu_t: coprime e #[(mu / 'chi_t)%R]%CF. suffices dv_o_mu_t: #[(mu / 'chi_t)%R]%CF %| 'o(mu)%CF * 'o('chi_t)%CF. by rewrite (coprime_dvdr dv_o_mu_t) // coprimeMr o_mu co_e_lam. rewrite !cfDet_order_lin //; apply/dvdn_cforderP=> x Gx. rewrite invr_lin_char // !cfunE exprMn -rmorphXn {2}mulnC /=. by rewrite !(dvdn_cforderP _) ?conjC1 ?mulr1 // dvdn_mulr. have /eqP mu_t_1: mu / 'chi_t == 1. rewrite -(dvdn_cforder (_ / _)%R 1) -(eqnP co_e_mu_t) dvdn_gcd dvdnn andbT. rewrite -(cfQuoK nsNG kerN_mu_t) cforder_mod // /e -card_quotient //. by rewrite cforder_lin_char_dvdG ?cfQuo_lin_char ?rpred_div. by apply: irr_inj; rewrite -['chi_t]mul1r -mu_t_1 divrK. 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)