proposition: Lemma odd_induced_orthogonal t : H <| G -> odd #|G| -> t != 0 -> '['Ind[G, H] 'chi_t, ('Ind[G] 'chi_t)^*] = 0.
proof: Proof. move=> nsHG oddG nz_t; have [sHG _] := andP nsHG. have:= cfclass_Ind_cases t (conjC_Iirr t) nsHG. rewrite conjC_IirrE conj_cfInd; case: cfclassP => // [[g Gg id_cht]]. have oddH: odd #|H| := pgroup.oddSg sHG oddG. case/eqP: nz_t; apply: irr_inj; rewrite irr0. apply/eqP; rewrite -odd_eq_conj_irr1 // id_cht; apply/eqP. have F1: ('chi_t ^ (g ^+ 2))%CF = 'chi_t. rewrite (cfConjgM _ nsHG) // -id_cht -conj_cfConjg -id_cht. exact: cfConjCK. suffices /eqP->: g == ((g ^+ 2) ^+ #|G|./2.+1)%g. elim: _./2.+1 => [|n IHn]; first exact: cfConjgJ1. by rewrite expgS (cfConjgM _ nsHG) ?groupX // F1. rewrite eq_mulVg1 expgS -expgM mul2n -mulgA mulKg -expgS -order_dvdn. by rewrite -add1n -[1%N](congr1 nat_of_bool oddG) odd_double_half order_dvdG. 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)