proposition: Lemma irr_reg_off_ker_0 t g : g \in G -> H <| G -> ~~ (H \subset cfker 'chi[G]_t) -> 'C_H[g] = 1%g -> 'chi_t g = 0.
proof: Proof. pose kerH i := H \subset cfker 'chi[G]_i => Gg nsHG kerH't regHg; apply/eqP. pose sum_norm2 x := \sum_i `|'chi_i x| ^+ 2. have norm2_ge0 a: 0 <= `|a| ^+ 2 :> algC by rewrite exprn_ge0 ?normr_ge0. have{regHg}: sum_norm2 gT G g <= sum_norm2 _ (G / H)%G (coset H g). rewrite ![sum_norm2 _ _ _](eq_bigr _ (fun _ _ => normCK _)). rewrite !second_orthogonality_relation ?mem_quotient // !class_refl ler_nat. suffices /card_isog->: 'C_G[g] \isog 'C_G[g] / H. exact/subset_leq_card/quotient_subcent1. by apply/quotient_isog; rewrite ?subIset 1?normal_norm // setICA regHg setIg1. rewrite /sum_norm2 (bigID kerH) ?sum_norm_irr_quo //= -lerBrDl subrr. rewrite le_eqVlt psumr_eq0 ?le_gtF ?sumr_ge0 // orbF => /allP/(_ t)/implyP. by rewrite mem_index_enum kerH't expf_eq0 normr_eq0. 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)