proposition: Theorem generalized_orthogonality_relation y (i j : Iirr G) : #|G|%:R^-1 * (\sum_(x in G) 'chi_i (x * y)%g * 'chi_j x^-1%g) = (i == j)%:R * ('chi_i y / 'chi_i 1%g).
proof: Proof. pose W := @socle_of_Iirr _ G; pose e k := Wedderburn_id (W k). pose aG := regular_repr algC G. have [Gy | notGy] := boolP (y \in G); last first. rewrite cfun0 // mul0r big1 ?mulr0 // => x Gx. by rewrite cfun0 ?groupMl ?mul0r. transitivity (('chi_i).[e j *m aG y]%CF / 'chi_j 1%g). rewrite [e j]Wedderburn_id_expansion -scalemxAl xcfunZr -mulrA; congr (_ * _). rewrite mulmx_suml raddf_sum big_distrl; apply: eq_bigr => x Gx /=. rewrite -scalemxAl xcfunZr -repr_mxM // xcfunG ?groupM // mulrAC mulrC. by congr (_ * _); rewrite mulrC mulKf ?irr1_neq0. rewrite mulr_natl mulrb; have [<-{j} | neq_ij] := eqVneq. by congr (_ / _); rewrite xcfun_mul_id ?envelop_mx_id ?xcfunG. rewrite (xcfun_annihilate neq_ij) ?mul0r //. case/andP: (Wedderburn_ideal (W j)) => _; apply: submx_trans. by rewrite mem_mulsmx ?Wedderburn_id_mem ?envelop_mx_id. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun eqtype choice ssrnat seq) mathcomp(path div fintype tuple finfun bigop prime order) mathcomp(ssralg poly finset gproduct fingroup morphism) mathcomp(perm automorphism quotient finalg action zmodp) mathcomp(commutator cyclic center pgroup nilpotent sylow) mathcomp(abelian matrix mxalgebra mxpoly mxrepresentation) mathcomp(vector ssrnum algC classfun archimedean)