proposition: Theorem gring_classM_expansion i j : 'K_i *m 'K_j = \sum_k (a i j k)%:R *: 'K_k.
proof: Proof. have [/imsetP[zi Gzi dKi] /imsetP[zj Gzj dKj]] := (enum_valP i, enum_valP j). pose aG := regular_repr F G; have sKG := subsetP (class_subG _ (subxx G)). transitivity (\sum_(x in zi ^: G) \sum_(y in zj ^: G) aG (x * y)%g). rewrite mulmx_suml -/aG dKi; apply: eq_bigr => x /sKG Gx. rewrite mulmx_sumr -/aG dKj; apply: eq_bigr => y /sKG Gy. by rewrite repr_mxM ?Gx ?Gy. pose h2 xy : gT := (xy.1 * xy.2)%g. pose h1 xy := enum_rank_in (classes1 G) (h2 xy ^: G). rewrite pair_big (partition_big h1 xpredT) //=; apply: eq_bigr => k _. rewrite (partition_big h2 [in enum_val k]) /= => [|[x y]]; last first. case/andP=> /andP[/= /sKG Gx /sKG Gy] /eqP <-. by rewrite enum_rankK_in ?class_refl ?mem_classes ?groupM ?Gx ?Gy. rewrite scaler_sumr; apply: eq_bigr => g Kk_g; rewrite scaler_nat. rewrite (set_gring_classM_coef _ _ Kk_g) -sumr_const; apply: eq_big => [] [x y]. rewrite !inE /= dKi dKj /h1 /h2 /=; apply: andb_id2r => /eqP ->. have /imsetP[zk Gzk dKk] := enum_valP k; rewrite dKk in Kk_g. by rewrite (class_eqP Kk_g) -dKk enum_valK_in eqxx andbT. by rewrite /h2 /= => /andP[_ /eqP->]. 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)