proposition: Theorem constt_Ind_mul_ext f (phi := 'chi_f) (psi := phi * theta) : G \subset 'I[phi] -> psi \in irr N -> let calS := irr_constt ('Ind phi) in [/\ {in calS, forall b, 'chi_b * chi \in irr G}, {in calS &, injective mul_Iirr}, irr_constt ('Ind psi) =i [seq mul_Iirr b | b in calS] & 'Ind psi = \sum_(b in calS) '['Ind phi, 'chi_b] *: 'chi_(mul_Iirr b)].
proof: Proof. move=> IGphi irr_psi calS. have IGpsi: G \subset 'I[psi]. by rewrite (subset_trans _ (inertia_mul _ _)) // subsetI IGphi. pose e b := '['Ind[G] phi, 'chi_b]; pose d b g := '['chi_b * chi, 'chi_g * chi]. have Ne b: e b \in Num.nat by rewrite Cnat_cfdot_char ?cfInd_char ?irr_char. have egt0 b: b \in calS -> e b > 0 by rewrite natr_gt0. have DphiG: 'Ind phi = \sum_(b in calS) e b *: 'chi_b := cfun_sum_constt _. have DpsiG: 'Ind psi = \sum_(b in calS) e b *: 'chi_b * chi. by rewrite /psi -cNt cfIndM // DphiG mulr_suml. pose d_delta := [forall b in calS, forall g in calS, d b g == (b == g)%:R]. have charMchi b: 'chi_b * chi \is a character by rewrite rpredM ?irr_char. have [_]: '['Ind[G] phi] <= '['Ind[G] psi] ?= iff d_delta. pose sum_delta := \sum_(b in calS) e b * \sum_(g in calS) e g * (b == g)%:R. pose sum_d := \sum_(b in calS) e b * \sum_(g in calS) e g * d b g. have ->: '['Ind[G] phi] = sum_delta. rewrite DphiG cfdot_suml; apply: eq_bigr => b _; rewrite cfdotZl cfdot_sumr. by congr (_ * _); apply: eq_bigr => g; rewrite cfdotZr cfdot_irr conj_natr. have ->: '['Ind[G] psi] = sum_d. rewrite DpsiG cfdot_suml; apply: eq_bigr => b _. rewrite -scalerAl cfdotZl cfdot_sumr; congr (_ * _). by apply: eq_bigr => g _; rewrite -scalerAl cfdotZr conj_natr. have eMmono := mono_leif (ler_pM2l (egt0 _ _)). apply: leif_sum => b /eMmono->; apply: leif_sum => g /eMmono->. split; last exact: eq_sym. have /natrP[n Dd]: d b g \in Num.nat by rewrite Cnat_cfdot_char. have [Db | _] := eqP; rewrite Dd leC_nat // -ltC_nat -Dd Db cfnorm_gt0. by rewrite -char1_eq0 // cfunE mulf_neq0 ?irr1_neq0. rewrite -!cfdot_Res_l ?cfRes_Ind_invariant // !cfdotZl cfnorm_irr irrWnorm //. rewrite eqxx => /esym/forall_inP/(_ _ _)/eqfun_inP; rewrite /d /= => Dd. have irrMchi: {in calS, forall b, 'chi_b * chi \in irr G}. by move=> b Sb; rewrite /= irrEchar charMchi Dd ?eqxx. have injMchi: {in calS &, injective mul_Iirr}. move=> b g Sb Sg /(congr1 (fun s => '['chi_s, 'chi_(mul_Iirr g)]))/eqP. by rewrite cfnorm_irr !cfIirrE ?irrMchi ?Dd // pnatr_eq1; case: (b =P g). have{DpsiG} ->: 'Ind psi = \sum_(b in calS) e b *: 'chi_(mul_Iirr b). by rewrite DpsiG; apply: eq_bigr => b Sb; rewrite -scalerAl cfIirrE ?irrMchi. split=> // i; rewrite irr_consttE cfdot_suml; apply/idP/idP=> [|/imageP[b Sb ->]]. apply: contraR => N'i; rewrite big1 // => b Sb. rewrite cfdotZl cfdot_irr mulrb ifN_eqC ?mulr0 //. by apply: contraNneq N'i => ->; apply: image_f. rewrite gt_eqF // (bigD1 b) //= cfdotZl cfnorm_irr mulr1 ltr_wpDr ?egt0 //. apply: sumr_ge0 => g /andP[Sg _]; rewrite cfdotZl cfdot_irr. by rewrite mulr_ge0 ?ler0n ?natr_ge0. 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)