msymm — Mathlib

English

For μ a partition, msymm(μ) is the sum of monomials whose exponent multiset equals the parts of μ.

Русский

Для μ — разбиение, msymm(μ) есть сумма мономов, у которых мульти-множество степеней совпадает с частями μ.

LaTeX

$$$\\mathrm{msymm}_{\\sigma,R}(\\mu) = \\sum_{s \\in \\{ a \\in \\mathrm{Sym}(\\sigma,n) \\mid a.\\mathrm{ofSym}=\\mu \\}} (s.1.1.map X).\\mathrm{prod}$$$

Lean4

/-- The monomial symmetric `MvPolynomial σ R` with exponent set μ.
It is the sum over all the monomials in `MvPolynomial σ R` such that
the multiset of exponents is equal to the multiset of parts of μ. -/
def msymm (μ : n.Partition) : MvPolynomial σ R :=
  ∑ s : { a : Sym σ n // .ofSym a = μ }, (s.1.1.map X).prod

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