proposition: Lemma cfnorm_Res_leif H phi : H \subset G -> '['Res[H] phi] <= #|G : H|%:R * '[phi] ?= iff (phi \in 'CF(G, H)).
proof: Proof. move=> sHG; rewrite cfun_onE mulrCA natf_indexg // -mulrA mulKf ?neq0CG //. rewrite (big_setID H) (setIidPr sHG) /= addrC. rewrite (mono_leif (ler_pM2l _)) ?invr_gt0 ?gt0CG // -leifBLR -sumrB. rewrite big1 => [|x Hx]; last by rewrite !cfResE ?subrr. have ->: (support phi \subset H) = (G :\: H \subset [set x | phi x == 0]). rewrite subDset setUC -subDset; apply: eq_subset => x. by rewrite !inE (andb_idr (contraR _)) // => /cfun0->. rewrite (sameP subsetP forall_inP); apply: leif_0_sum => x _. by rewrite !inE /<?=%R mul_conjC_ge0 eq_sym mul_conjC_eq0. 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)