proposition: Lemma cfRes_irr_irr chi : chi \is a character -> 'Res[H] chi \in irr H -> chi \in irr G.
proof: Proof. have [sHG /char_reprP[rG ->] | not_sHG Nchi] := boolP (H \subset G). rewrite -(cfRepr_sub _ sHG) => /irr_reprP[rH irrH def_rH]; apply/irr_reprP. suffices /subg_mx_irr: mx_irreducible (subg_repr rG sHG) by exists rG. by apply: mx_rsim_irr irrH; apply/cfRepr_rsimP/eqP. rewrite cfResEout // => /irrP[j Dchi_j]; apply/lin_char_irr/cfRes_lin_lin=> //. suffices j0: j = 0 by rewrite cfResEout // Dchi_j j0 irr0 rpred1. apply: contraNeq (irr1_neq0 j) => nz_j. have:= xcfun_id j 0; rewrite -Dchi_j cfunE xcfunZl -irr0 xcfun_id eqxx => ->. by rewrite (negPf nz_j). Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun eqtype choice ssrnat seq) mathcomp(path div fintype tuple finfun bigop prime order) mathcomp(ssralg poly finset gproduct fingroup morphism) mathcomp(perm automorphism quotient finalg action zmodp) mathcomp(commutator cyclic center pgroup nilpotent sylow) mathcomp(abelian matrix mxalgebra mxpoly mxrepresentation) mathcomp(vector ssrnum algC classfun archimedean)