proposition: Lemma cfdotElr A B phi psi : phi \in 'CF(G, A) -> psi \in 'CF(G, B) -> '[phi, psi] = #|G|%:R^-1 * \sum_(x in A :&: B) phi x * (psi x)^*.
proof: Proof. move=> Aphi Bpsi; rewrite (big_setID G)/= cfdotE (big_setID (A :&: B))/= setIC. congr (_ * (_ + _)); rewrite !big1 // => x /setDP[_]. by move/cfun0->; rewrite mul0r. rewrite inE; case/nandP=> notABx; first by rewrite (cfun_on0 Aphi) ?mul0r. by rewrite (cfun_on0 Bpsi) // rmorph0 mulr0. 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 finalg action gproduct) mathcomp(zmodp commutator cyclic center pgroup sylow) mathcomp(matrix vector falgebra ssrnum algC algnum) mathcomp(archimedean)