# mathlibdocumentation

ring_theory.polynomial.symmetric

# Symmetric Polynomials and Elementary Symmetric Polynomials #

This file defines symmetric mv_polynomials and elementary symmetric mv_polynomials. We also prove some basic facts about them.

## Main declarations #

• mv_polynomial.is_symmetric

• mv_polynomial.symmetric_subalgebra

• mv_polynomial.esymm

## Notation #

• esymm σ R n, is the nth elementary symmetric polynomial in mv_polynomial σ R.

As in other polynomial files, we typically use the notation:

• σ τ : Type* (indexing the variables)

• R S : Type* [comm_semiring R] [comm_semiring S] (the coefficients)

• r : R elements of the coefficient ring

• i : σ, with corresponding monomial X i, often denoted X_i by mathematicians

• φ ψ : mv_polynomial σ R

def multiset.esymm {R : Type u_1} (s : multiset R) (n : ) :
R

The nth elementary symmetric function evaluated at the elements of s

Equations
def mv_polynomial.is_symmetric {σ : Type u_1} {R : Type u_2} (φ : R) :
Prop

A mv_polynomial φ is symmetric if it is invariant under permutations of its variables by the rename operation

Equations
def mv_polynomial.symmetric_subalgebra (σ : Type u_1) (R : Type u_2)  :
R)

The subalgebra of symmetric mv_polynomials.

Equations
@[simp]
theorem mv_polynomial.mem_symmetric_subalgebra {σ : Type u_1} {R : Type u_2} (p : R) :
@[simp]
theorem mv_polynomial.is_symmetric.C {σ : Type u_1} {R : Type u_2} (r : R) :
@[simp]
theorem mv_polynomial.is_symmetric.zero {σ : Type u_1} {R : Type u_2}  :
@[simp]
theorem mv_polynomial.is_symmetric.one {σ : Type u_1} {R : Type u_2}  :
theorem mv_polynomial.is_symmetric.add {σ : Type u_1} {R : Type u_2} {φ ψ : R} (hφ : φ.is_symmetric) (hψ : ψ.is_symmetric) :
+ ψ).is_symmetric
theorem mv_polynomial.is_symmetric.mul {σ : Type u_1} {R : Type u_2} {φ ψ : R} (hφ : φ.is_symmetric) (hψ : ψ.is_symmetric) :
* ψ).is_symmetric
theorem mv_polynomial.is_symmetric.smul {σ : Type u_1} {R : Type u_2} {φ : R} (r : R) (hφ : φ.is_symmetric) :
@[simp]
theorem mv_polynomial.is_symmetric.map {σ : Type u_1} {R : Type u_2} {S : Type u_4} {φ : R} (hφ : φ.is_symmetric) (f : R →+* S) :
theorem mv_polynomial.is_symmetric.neg {σ : Type u_1} {R : Type u_2} [comm_ring R] {φ : R} (hφ : φ.is_symmetric) :
theorem mv_polynomial.is_symmetric.sub {σ : Type u_1} {R : Type u_2} [comm_ring R] {φ ψ : R} (hφ : φ.is_symmetric) (hψ : ψ.is_symmetric) :
- ψ).is_symmetric
noncomputable def mv_polynomial.esymm (σ : Type u_1) (R : Type u_2) [fintype σ] (n : ) :

The nth elementary symmetric mv_polynomial σ R.

Equations
theorem mv_polynomial.esymm_eq_multiset.esymm (σ : Type u_1) (R : Type u_2) [fintype σ] (n : ) :
n = (multiset.map (λ (i : σ), finset.univ.val).esymm n

The nth elementary symmetric mv_polynomial σ R is obtained by evaluating the nth elementary symmetric at the multiset of the monomials

theorem mv_polynomial.esymm_eq_sum_subtype (σ : Type u_1) (R : Type u_2) [fintype σ] (n : ) :
n = finset.univ.sum (λ (t : {s // s.card = n}), t.prod (λ (i : σ),

We can define esymm σ R n by summing over a subtype instead of over powerset_len.

theorem mv_polynomial.esymm_eq_sum_monomial (σ : Type u_1) (R : Type u_2) [fintype σ] (n : ) :
n = (λ (t : finset σ), (mv_polynomial.monomial (t.sum (λ (i : σ), 1))) 1)

We can define esymm σ R n as a sum over explicit monomials

@[simp]
theorem mv_polynomial.esymm_zero (σ : Type u_1) (R : Type u_2) [fintype σ] :
0 = 1
theorem mv_polynomial.map_esymm (σ : Type u_1) (R : Type u_2) {S : Type u_4} [fintype σ] (n : ) (f : R →+* S) :
n) = n
theorem mv_polynomial.rename_esymm (σ : Type u_1) (R : Type u_2) {τ : Type u_3} [fintype σ] [fintype τ] (n : ) (e : σ τ) :
n) = n
theorem mv_polynomial.esymm_is_symmetric (σ : Type u_1) (R : Type u_2) [fintype σ] (n : ) :
theorem mv_polynomial.support_esymm'' (σ : Type u_1) (R : Type u_2) [fintype σ] (n : ) [decidable_eq σ] [nontrivial R] :
n).support = (λ (t : finset σ), (finsupp.single (t.sum (λ (i : σ), 1)) 1).support)
theorem mv_polynomial.support_esymm' (σ : Type u_1) (R : Type u_2) [fintype σ] (n : ) [decidable_eq σ] [nontrivial R] :
n).support = (λ (t : finset σ), {t.sum (λ (i : σ), 1)})
theorem mv_polynomial.support_esymm (σ : Type u_1) (R : Type u_2) [fintype σ] (n : ) [decidable_eq σ] [nontrivial R] :
n).support = finset.image (λ (t : finset σ), t.sum (λ (i : σ), 1))
theorem mv_polynomial.degrees_esymm (σ : Type u_1) (R : Type u_2) [fintype σ] [nontrivial R] (n : ) (hpos : 0 < n) (hn : n ) :