proposition: Fact homogsym_vecaxiom : vector_axiom #|[set p : 'P_d | (size p <= n)%N]| {homsym R[n, d]}.
proof: Proof. pose b := [set p : 'P_d | (size p <= n)%N]. pose t := enum_tuple (pred_of_set b). have sztntht k : (size (tnth t k) <= n)%N. by have := mem_tnth k t; rewrite /t mem_enum inE. exists (fun p : {homsym R[n, d]} => \row_(i < #|b|) p@_(mpart (tnth t i))). by move=> c p q; apply/matrixP=> i j; rewrite !mxE /= mcoeffD mcoeffZ. exists (fun r : 'rV[R]_(#|b|) => \sum_(i < #|b|) (r ord0 i) *: (homsymm (tnth t i))). - move=> p; rewrite [RHS]homsymmE. rewrite (bigID (mem b)) /= [X in _ + X]big1 ?addr0 => [|la]; first last. rewrite inE => /negbTE H . by apply val_inj; apply val_inj; rewrite /= /symm H scaler0. rewrite [RHS](eq_bigl (fun la => la \in b)); first last. by move=> i /=; rewrite inE. rewrite -[RHS]big_enum /= -[enum _]/(tval t). rewrite big_tuple; apply eq_bigr => i _; congr (_ *: _). by rewrite mxE. - move=> r /=; apply/matrixP=> i j. rewrite mxE !raddf_sum ord1 /= (bigD1 j) //=. rewrite !linearZ /= mcoeff_symm ?sztntht //. rewrite perm_refl mulr1 big1 ?addr0 //. move=> k Hkj. rewrite !linearZ /= mcoeff_symm ?sztntht //. suff : ~~(perm_eq (mpart (n := n) (tnth t k)) (mpart (n := n) (tnth t j))). by move /negbTE ->; rewrite mulr0. move: Hkj; apply contra => /perm_partm/(congr1 val)/eqP. rewrite /= !mpartK // !(tnth_nth (rowpartn d)) /t /= => H. apply/eqP/val_inj/eqP => /=. by rewrite -(nth_uniq (rowpartn d) _ _ (enum_uniq (pred_of_set b))) // -cardE. 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