Elementary symmetric polynomials in small finite alphabets #
This file gives explicit formulas for elementary symmetric polynomials in small finite alphabets.
Such expansions support explicit computations of symmetric orbit products. In particular, the
four-variable formula is used to express the quartic D₄ resolvent's orbit product in elementary
symmetric polynomials.
Main results #
TauCeti.esymm_fin_four: the four elementary symmetric polynomials in four variables.
theorem
TauCeti.esymm_fin_four
{R : Type u_1}
[CommSemiring R]
:
MvPolynomial.esymm (Fin 4) R 1 = MvPolynomial.X 0 + MvPolynomial.X 1 + MvPolynomial.X 2 + MvPolynomial.X 3 ∧ MvPolynomial.esymm (Fin 4) R 2 = MvPolynomial.X 0 * MvPolynomial.X 1 + MvPolynomial.X 0 * MvPolynomial.X 2 + MvPolynomial.X 0 * MvPolynomial.X 3 + MvPolynomial.X 1 * MvPolynomial.X 2 + MvPolynomial.X 1 * MvPolynomial.X 3 + MvPolynomial.X 2 * MvPolynomial.X 3 ∧ MvPolynomial.esymm (Fin 4) R 3 = MvPolynomial.X 0 * MvPolynomial.X 1 * MvPolynomial.X 2 + MvPolynomial.X 0 * MvPolynomial.X 1 * MvPolynomial.X 3 + MvPolynomial.X 0 * MvPolynomial.X 2 * MvPolynomial.X 3 + MvPolynomial.X 1 * MvPolynomial.X 2 * MvPolynomial.X 3 ∧ MvPolynomial.esymm (Fin 4) R 4 = MvPolynomial.X 0 * MvPolynomial.X 1 * MvPolynomial.X 2 * MvPolynomial.X 3
The elementary symmetric polynomials in four variables, written out explicitly.