Coefficients of symmetric polynomials in two variables #
A polynomial f(X, Y) is symmetric when it is fixed by every permutation of its variables
(MvPolynomial.IsSymmetric). For two variables this says f(X, Y) = f(Y, X), which this file
records coefficientwise.
Main results #
MvPolynomial.IsSymmetric.coeff_single_add_single: the coefficients of a symmetric two-variable polynomial are symmetric.
theorem
MvPolynomial.IsSymmetric.coeff_single_add_single
{R : Type u_1}
[CommSemiring R]
{f : MvPolynomial (Fin 2) R}
(hs : f.IsSymmetric)
(i j : ℕ)
:
f.coeff (Finsupp.single 0 i + Finsupp.single 1 j) = f.coeff (Finsupp.single 0 j + Finsupp.single 1 i)
The coefficients of a symmetric two-variable polynomial are symmetric: the coefficient of
XⁱYʲ equals that of XʲYⁱ.