mathlib3 documentation

ring_theory.mv_polynomial.symmetric

Symmetric Polynomials and Elementary Symmetric Polynomials #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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 multiset.esymm {R : Type u_1} [comm_semiring R] (s : multiset R) (n : ) :
R

The nth elementary symmetric function evaluated at the elements of s

Equations
theorem finset.esymm_map_val {R : Type u_1} [comm_semiring R] {σ : Type u_2} (f : σ R) (s : finset σ) (n : ) :
(multiset.map f s.val).esymm n = (finset.powerset_len n s).sum (λ (t : finset σ), t.prod f)
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
noncomputable def mv_polynomial.esymm (σ : Type u_1) (R : Type u_2) [comm_semiring R] [fintype σ] (n : ) :

The nth elementary symmetric mv_polynomial σ R.

Equations

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) [comm_semiring R] [fintype σ] (n : ) :
mv_polynomial.esymm σ R n = finset.univ.sum (λ (t : {s // s.card = n}), t.prod (λ (i : σ), 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.support_esymm'' (σ : Type u_1) (R : Type u_2) [comm_semiring R] [fintype σ] (n : ) [decidable_eq σ] [nontrivial R] :
theorem mv_polynomial.support_esymm' (σ : Type u_1) (R : Type u_2) [comm_semiring R] [fintype σ] (n : ) [decidable_eq σ] [nontrivial R] :
(mv_polynomial.esymm σ R n).support = (finset.powerset_len n finset.univ).bUnion (λ (t : finset σ), {t.sum (λ (i : σ), finsupp.single i 1)})
theorem mv_polynomial.support_esymm (σ : Type u_1) (R : Type u_2) [comm_semiring R] [fintype σ] (n : ) [decidable_eq σ] [nontrivial R] :
theorem mv_polynomial.degrees_esymm (σ : Type u_1) (R : Type u_2) [comm_semiring R] [fintype σ] [nontrivial R] (n : ) (hpos : 0 < n) (hn : n fintype.card σ) :