Ssreflect Users Discussion List

[Florent Hivert <>]

      Dear Ssreflect fan,

In his development on multivariate polynomials Pierre-Yves Strub, proved two
theorems that essentially says that the ring of symmetric polynomials in n
variable is isomorphic to the ring of polynomials in the elementary symmetric
polynomials (the fundamental theorem of symmetric polynomials):

1) Any polynomial p is a polynomials in the elementary ones:

p \mPo lq == multivariate polynomial composition
's_(n, k) == the k-th elementary symmetric polynomial with n indeterminates.

S := [tuple 's_(R, n, i.+1) | i < n].
Lemma sym_fundamental (p : {mpoly R[n]}) : p \is symmetric ->
  { t | t \mPo S = p /\ mweight t <= msize p}.

2) The polynomial is unique:

Lemma msym_fundamental_un (t1 t2 : {mpoly R[n]}) :
  t1 \mPo S = t2 \mPo S -> t1 = t2.

As a consequence, the family ('S_l)_l where l goes along the sets of 
partitions
(sorted list of non negative integer called the part) in parts at most n is a
linear basis of the space of symmetric polynomials. I'd like to state this
fact, and to give some other bases. I need some advice. Here is my precise
question:

It looks that the library vector.v is the tools for speaking of
subspace. However it is only tailored to finite dimensional
spaces. Theoretically, I can restrict to polynomials of bounded degree or to
homogeneous polynomials but I've no idea if it will be practical. Any
suggestions ?

Regards,

Florent