Theorems · Definition · commutative algebra

MvPolynomial.esymm

(σ : Type u_5) → (R : Type u_6) → [inst : CommSemiring R] → [Fintype σ] → ℕ → MvPolynomial σ R

The nth elementary symmetric MvPolynomial σ R. It is the sum over all the degree n squarefree monomials in MvPolynomial σ R.

Defined in

Mathlib.RingTheory.MvPolynomial.Symmetric.Defs

Cited by

31 results in Mathlib

Foundations

Depth 84 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

CommSemiringFintype