proposition: Lemma equiv_restrict_compl_ortho A m (Phi : m.-tuple 'CF(H)) mu_ : H \subset G -> A <| H -> basis_of 'CF(H, A) Phi -> (forall i j, '[mu_ i, mu_ j] = (i == j)%:R) -> (forall j : 'I_m, 'Ind[G] Phi`_j = \sum_i '[Phi`_j, 'chi_i] *: mu_ i) -> [/\ forall i, {in A, mu_ i =1 'chi_i} & forall mu, (forall i, '[mu, mu_ i] = 0) -> {in A, forall x, mu x = 0}].
proof: Proof. move=> HsG nsAH /equiv_restrict_compl Phi_A Mo IP; split=> [/= i | mu Cmu x Ax]. have->: 'chi[H]_i = \sum_j (j == i)%:R *: 'chi_j. rewrite (bigD1 i) //= eqxx scale1r big1 ?addr0 // => j /negPf->. by rewrite scale0r. apply/Phi_A=> // j; rewrite IP cfdot_suml. by apply: eq_bigr=> k _; rewrite cfdotZl rmorph_nat Mo. transitivity ((\sum_j 0 *: 'chi[H]_j) x); last first. by rewrite sum_cfunE big1 // => j _; rewrite cfunE mul0r. move: x Ax; apply/Phi_A=> // j. rewrite -mulr_suml rmorph0 mulr0 IP cfdot_suml big1 // => k _. by rewrite cfdotZl [d in _ * d]cfdotC Cmu rmorph0 mulr0. 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)