proposition: Lemma homsymdotC p q : '[p | q] = ('[q | p])^*.
proof: Proof. rewrite /homsymdot rmorph_sum /=. apply: eq_bigr=> x _. rewrite [in RHS]rmorphM [X in _ = X * _]rmorphM conjCK -!mulrA. have /geC0_conj -> : 0 <= ((zcard (enum_val x))%:R : algC). by rewrite -nnegrE ?nnegrE ?ler01 ?ler0n ?oner_neq0. by congr (_ * _); rewrite mulrC. Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(ssralg matrix vector ssrnum algC archimedean) mathcomp(fingroup perm) mathcomp(ssrcomplements freeg mpoly) tools sorted ordtype permuted partition permcent antisym Schur_mpoly Schur_altdef sympoly