proposition: Corollary constt_Ind_ext : [/\ forall b : Iirr (G / N), 'chi_(mod_Iirr b) * chi \in irr G, injective mul_mod_Iirr, irr_constt ('Ind theta) =i codom mul_mod_Iirr & 'Ind theta = \sum_b 'chi_b 1%g *: 'chi_(mul_mod_Iirr b)].
proof: Proof. have IHchi0: G \subset 'I['chi[N]_0] by rewrite inertia_irr0. have [] := constt_Ind_mul_ext IHchi0; rewrite irr0 ?mul1r ?mem_irr //. set psiG := 'Ind 1 => irrMchi injMchi constt_theta {2}->. have dot_psiG b: '[psiG, 'chi_(mod_Iirr b)] = 'chi[G / N]_b 1%g. rewrite mod_IirrE // -cfdot_Res_r cfRes_sub_ker ?cfker_mod //. by rewrite cfdotZr cfnorm1 mulr1 conj_natr ?cfMod1 ?Cnat_irr1. have mem_psiG (b : Iirr (G / N)): mod_Iirr b \in irr_constt psiG. by rewrite irr_consttE dot_psiG irr1_neq0. have constt_psiG b: (b \in irr_constt psiG) = (N \subset cfker 'chi_b). apply/idP/idP=> [psiGb | /quo_IirrK <- //]. by rewrite constt0_Res_cfker // -constt_Ind_Res irr0. split=> [b | b g /injMchi/(can_inj (mod_IirrK nsNG))-> // | b0 | ]. - exact: irrMchi. - rewrite constt_theta. apply/imageP/imageP=> [][b psiGb ->]; last by exists (mod_Iirr b). by exists (quo_Iirr N b) => //; rewrite /mul_mod_Iirr quo_IirrK -?constt_psiG. rewrite (reindex_onto _ _ (in1W (mod_IirrK nsNG))) /=. apply/esym/eq_big => b; first by rewrite constt_psiG quo_IirrKeq. by rewrite -dot_psiG /mul_mod_Iirr => /eqP->. 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)