esymm — Mathlib

English

The nth elementary symmetric function esymm on a finite type σ over R is defined by summing the products of all n-element subsets from the powerset of univ.

Русский

Пусть σ — конечный тип. n-ая элементарная симметрическая функция esymm на σ над R определяется как сумма произведений всех n-элементных подп множеств из полного множества.

LaTeX

$$def esymm (n : ℕ) : MvPolynomial σ R := ∑ t ∈ powersetCard n univ, ∏ i ∈ t, X i$$

Lean4

/-- The `n`th elementary symmetric `MvPolynomial σ R`.
It is the sum over all the degree n squarefree monomials in `MvPolynomial σ R`. -/
def esymm (n : ℕ) : MvPolynomial σ R :=
  ∑ t ∈ powersetCard n univ, ∏ i ∈ t, X i

Похожие утверждения