proposition: Lemma homsymdot_omegasf f g : (d <= n)%N -> '[ omegahomsym f | omegahomsym g ] = '[ f | g ].
proof: Proof. move=> Hd; have /andP[/eqP Hfull Hfree]:= symbp_basis Hd char0_algC. have:= (memvf g); rewrite -Hfull => /coord_span ->. rewrite raddf_sum /= !homsymdot_sumr; apply eq_bigr => i _. have:= (memvf f); rewrite -Hfull => /coord_span ->. rewrite raddf_sum /= !homsymdot_suml; apply eq_bigr => j _. rewrite !linearZ /= !homsymdotZl !homsymdotZr; congr (_ * (_ * _)). rewrite ![_`_i](nth_map (rowpartn d)) -?cardE //. rewrite ![_`_j](nth_map (rowpartn d)) -?cardE //. rewrite !omega_homsymp //; try by apply: (leq_trans (leq_head_sumn _)); rewrite sumn_intpartn. rewrite homsymdotZl homsymdotZr !homsymdotpp //. case: eqP => /= [->|_]; rewrite ?mulr0 // !mulr1 !mulrA. move: (nth _ _ _) => la {i j}. have /Num.Theory.conj_intr -> : (-1) ^+ (d - size la) \in (@archimedean.Num.int algC) by apply rpred_sign. by rewrite -exprD addnn -muln2 exprM sqrr_sign mul1r. 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