proposition: Theorem second_orthogonality_relation x y : y \in G -> \sum_i 'chi[G]_i x * ('chi_i y)^* = #|'C_G[x]|%:R *+ (x \in y ^: G).
proof: Proof. move=> Gy; pose i_x := iC (x ^: G); pose i_y := iC (y ^: G). have [Gx | notGx] := boolP (x \in G); last first. rewrite (contraNF (subsetP _ x) notGx) ?class_subG ?big1 // => i _. by rewrite cfun0 ?mul0r. transitivity ((#|'C_G[repr (y ^: G)]|%:R *: (X' *m X)) i_y i_x). rewrite scalemxAl !mxE; apply: eq_bigr => k _; rewrite !mxE mulrC -!mulrA. by rewrite !class_IirrK ?mem_classes // !cfun_repr mulVKf ?neq0CG. rewrite mulmx1C // !mxE -!divg_index !(index_cent1, =^~ indexgI). rewrite (class_eqP (mem_repr y _)) ?class_refl // mulr_natr. rewrite (can_in_eq class_IirrK) ?mem_classes //. have [-> | not_yGx] := eqVneq; first by rewrite class_refl. by rewrite [x \in _](contraNF _ not_yGx) // => /class_eqP->. 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)