proposition: Lemma Aint_gring_mode_class_sum k : 'omega_i['K_k] \in Aint.
proof: Proof. move: k; pose X := [tuple 'omega_i['K_k] | k < #|classes G| ]. have memX k: 'omega_i['K_k] \in X by apply: image_f. have S_P := Cint_spanP X; set S := Cint_span X in S_P. have S_X: {subset X <= S} by apply: mem_Cint_span. have S_1: 1 \in S. apply: S_X; apply/codomP; exists (enum_rank_in (classes1 G) 1%g). rewrite (@gring_mode_class_sum_eq _ 1%g) ?enum_rankK_in ?classes1 //. by rewrite mulfK ?irr1_neq0 // class1G cards1. suffices Smul: mulr_closed S. by move=> k; apply: fin_Csubring_Aint S_P _ _; rewrite ?S_X. split=> // _ _ /S_P[x ->] /S_P[y ->]. rewrite mulr_sumr rpred_sum // => j _. rewrite mulrzAr mulr_suml rpredMz ?rpred_sum // => k _. rewrite mulrzAl rpredMz {x y}// !nth_mktuple. rewrite -gring_irr_modeM ?gring_class_sum_central //. rewrite gring_classM_expansion raddf_sum rpred_sum // => jk _. by rewrite scaler_nat raddfMn rpredMn ?S_X ?memX. 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)