proposition: Lemma cfdot_dprod phi1 phi2 psi1 psi2 : '[cfDprod phi1 psi1, cfDprod phi2 psi2] = '[phi1, phi2] * '[psi1, psi2].
proof: Proof. rewrite !cfdotE mulrCA -mulrA mulrCA mulrA -invfM -natrM (dprod_card KxH). congr (_ * _); rewrite big_distrl reindex_dprod /=; apply: eq_bigr => k Kk. rewrite big_distrr; apply: eq_bigr => h Hh /=. by rewrite mulrCA -mulrA -rmorphM mulrCA mulrA !cfDprodE. 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)