proposition: Lemma equiv_restrict_compl A m (Phi : m.-tuple 'CF(H)) (mu : 'CF(G)) d : H \subset G -> A <| H -> basis_of 'CF(H, A) Phi -> ({in A, mu =1 \sum_i d i *: 'chi_i} <-> (forall j : 'I_m, \sum_i '[Phi`_j, 'chi_i] * (d i)^* = '['Ind[G] Phi`_j, mu])).
proof: Proof. move=> sHG nsAH BPhi; have [sAH nAH] := andP nsAH. have APhi (i : 'I_m) : Phi`_i \in 'CF(H, A). by apply: (basis_mem BPhi _); apply: mem_nth; rewrite size_tuple. pose D := 'Res[H] mu - \sum_i d i *: 'chi_i. transitivity (D \in 'CF(H, H :\: A)). split=> [A'D | /cfun_onP A'D x Ax]. apply/cfun_onP=> x; rewrite inE negb_and negbK. case/orP=> [Ax | /cfun0-> //]; rewrite !cfunE -A'D //. by rewrite cfResE ?subrr ?(subsetP sAH). have:= A'D x; rewrite !cfunE !inE Ax => /(_ isT)/(canRL (subrK _)). by rewrite add0r cfResE // ?(subsetP sAH). have F0 (j : 'I_m) : (\sum_i '[Phi`_j, 'chi_i] * (d i)^* == '['Ind Phi`_j, mu]) = ('[Phi`_j, D] == 0). rewrite raddfB raddf_sum /= Frobenius_reciprocity subr_eq0 eq_sym. by congr (_ == _); apply: eq_bigr=> i _; rewrite cfdotZr mulrC. split=> [HH j | HH]. by apply/eqP; rewrite F0; apply/eqP; apply: cfdot_complement. have{F0} F1 (j : 'I_m) : '[Phi`_j, D]_H = 0. by have/eqP := HH j; rewrite F0 => /eqP. have: (D \in 'CF(H))%VS by rewrite memvf. rewrite -(cfun_complement nsAH) => /memv_addP[f Cf [g Cg defD]]. have: '[f, f + g] = 0. rewrite -defD (coord_basis BPhi Cf) cfdot_suml. by rewrite big1 // => i _; rewrite cfdotZl F1 mulr0. rewrite raddfD /= {1}(cfdot_complement Cf Cg) addr0 => /eqP. by rewrite cfnorm_eq0 defD => /eqP->; rewrite add0r. Qed.
imports: mathcomp.ssreflect.ssreflect mathcomp(ssrbool ssrfun eqtype ssrnat seq path div choice fintype) mathcomp(tuple finfun bigop prime order ssralg finset fingroup morphism) mathcomp(perm automorphism quotient action zmodp finalg center commutator) mathcomp(poly cyclic pgroup nilpotent matrix mxalgebra mxrepresentation) mathcomp(vector falgebra fieldext ssrnum algC rat algnum galois) mathcomp(classfun character inertia integral_char vcharacter)