mathlib documentation

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 #

Notation #

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

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

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

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

The nth elementary symmetric mv_polynomial σ R.

Equations
theorem mv_polynomial.esymm_eq_sum_subtype (σ : Type u_1) (R : Type u_2) [comm_semiring R] [fintype σ] (n : ) :
mv_polynomial.esymm σ R n = ∑ (t : {s // s.card = n}), ∏ (i : σ) in t, mv_polynomial.X 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) [comm_semiring R] [fintype σ] (n : ) :

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) [comm_semiring R] [fintype σ] :
theorem mv_polynomial.map_esymm (σ : Type u_1) (R : Type u_2) {S : Type u_4} [comm_semiring R] [comm_semiring S] [fintype σ] (n : ) (f : R →+* S) :
theorem mv_polynomial.rename_esymm (σ : Type u_1) (R : Type u_2) {τ : Type u_3} [comm_semiring R] [fintype σ] [fintype τ] (n : ) (e : σ τ) :
theorem mv_polynomial.esymm_is_symmetric (σ : Type u_1) (R : Type u_2) [comm_semiring R] [fintype σ] (n : ) :