proposition: Theorem nonlinear_irr_vanish gT (G : {group gT}) i : 'chi[G]_i 1%g > 1 -> exists2 x, x \in G & 'chi_i x = 0.
proof: Proof. move=> chi1gt1; apply/exists_eq_inP; apply: contraFT (lt_geF chi1gt1). move=> /exists_inPn-nz_chi. rewrite -(norm_natr (Cnat_irr1 i)) -(@expr_le1 _ 2)//. rewrite -(lerD2r (#|G|%:R * '['chi_i])) {1}cfnorm_irr mulr1. rewrite (cfnormE (cfun_onG _)) mulVKf ?neq0CG // (big_setD1 1%g) //=. rewrite addrCA lerD2l (cardsD1 1%g) group1 mulrS lerD2l. rewrite -sumr_const !(partition_big_imset (fun s => <[s]>)) /=. apply: ler_sum => _ /imsetP[g /setD1P[ntg Gg] ->]. have sgG: <[g]> \subset G by rewrite cycle_subG. pose S := [pred s | generator <[g]> s]; pose chi := 'Res[<[g]>] 'chi_i. have defS: [pred s in G^# | <[s]> == <[g]>] =i S. move=> s; rewrite inE /= eq_sym andb_idl // !inE -cycle_eq1 -cycle_subG. by move/eqP <-; rewrite cycle_eq1 ntg. have resS: {in S, 'chi_i =1 chi}. by move=> s /cycle_generator=> g_s; rewrite cfResE ?cycle_subG. rewrite !(eq_bigl _ _ defS) sumr_const. rewrite (eq_bigr (fun s => `|chi s| ^+ 2)) => [|s /resS-> //]. apply: sum_norm2_char_generators => [|s Ss]. by rewrite cfRes_char ?irr_char. by rewrite -resS // nz_chi ?(subsetP sgG) ?cycle_generator. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq path) mathcomp(div choice fintype tuple finfun bigop prime order) mathcomp(ssralg poly finset fingroup morphism perm) mathcomp(automorphism quotient action countalg finalg zmodp) mathcomp(commutator cyclic center pgroup sylow gseries) mathcomp(nilpotent abelian ssrnum ssrint archimedean polydiv) mathcomp(rat matrix mxalgebra intdiv mxpoly vector falgebra) mathcomp(fieldext separable galois algC cyclotomic algnum) mathcomp(mxrepresentation classfun character)