hsymm — Mathlib

English

The nth complete homogeneous symmetric polynomial hsymm(n) is the sum over all degree-n monomials arising from all degree-n multisets of σ, namely hsymm(n) = ∑_{s ∈ Sym(σ,n)} (s.1.map X).prod.

Русский

N-й полный однородный симметрический полином hsymm(n) — это сумма по всем мономиалам степени n, полученным из всех многолетних наборов σ: hsymm(n) = ∑_{s ∈ Sym(σ,n)} (s.1.map X).prod.

LaTeX

$$$ hsymm( n ) = \\sum s ∈ \\mathrm{Sym}(\\sigma,n), (s.1.map X).prod $$$

Lean4

/-- The `n`th complete homogeneous symmetric `MvPolynomial σ R`.
It is the sum over all the degree n monomials in `MvPolynomial σ R`. -/
def hsymm (n : ℕ) : MvPolynomial σ R :=
  ∑ s : Sym σ n, (s.1.map X).prod

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