proposition: Lemma vchar_ker_mod_prim : {in G & G & 'Z[irr G], forall x y (chi : 'CF(G)), #[x] = p -> y \in 'C[x] -> chi (x * y)%g == chi y %[mod e]}%A.
proof: Proof. move=> x y chi Gx Gy Zchi ox cxy; pose X := <<[set x; y]>>%G. have [Xx Xy]: x \in X /\ y \in X by apply/andP; rewrite -!sub1set -join_subG. have sXG: X \subset G by rewrite join_subG !sub1set Gx. suffices{chi Zchi} IHiX i: ('chi[X]_i (x * y)%g == 'chi_i y %[mod e])%A. rewrite -!(cfResE _ sXG) ?groupM //. have irr_free := (free_uniq (basis_free (irr_basis X))). have [c Zc ->] := (zchar_expansion irr_free (cfRes_vchar X Zchi)). rewrite !sum_cfunE /eqAmod -sumrB big_seq rpred_sum // => _ /irrP[i ->]. by rewrite !cfunE [(_ %| _)%A]eqAmodMl // rpred_Cint. have lin_chi: 'chi_i \is a linear_char. apply/char_abelianP; rewrite -[gval X]joing_idl -joing_idr abelianY. by rewrite !cycle_abelian cycle_subG /= cent_cycle. rewrite lin_charM // -{2}['chi_i y]mul1r eqAmodMr ?Aint_irr //. have [|k ->] := (prim_rootP pr_eps) ('chi_i x). by rewrite -lin_charX // -ox expg_order lin_char1. rewrite -[_ ^+ k](subrK 1) subrX1 -[_ - 1]opprB mulNr -mulrN mulrC. rewrite eqAmod_addl_mul // rpredN rpred_sum // => n _. by rewrite rpredX ?(Aint_prim_root pr_eps). 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)