proposition: Lemma cfdot_complement A phi psi : phi \in 'CF(G, A) -> psi \in 'CF(G, G :\: A) -> '[phi, psi] = 0.
proof: Proof. move=> Aphi A'psi; rewrite (cfdotElr Aphi A'psi). by rewrite setDE setICA setICr setI0 big_set0 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)