psumPart — Mathlib

English

For a partition μ of n, psumPart(μ) is the product of psum(μ_i) over all parts μ_i of μ.

Русский

Для разложения μ на части μ_i, psumPart(μ) равен произведению psum(μ_i) по всем частям μ.

LaTeX

$$$\\mathrm{psumPart}_{\\sigma,R}(\\mu) = \\prod_{a \\in \\mu.\\mathrm{parts}} \\mathrm{psum}_{\\sigma,R}(a)$$$

Lean4

/-- `psumPart` is the product of the symmetric polynomials `psum μᵢ`,
where `μ = (μ₁, μ₂, ...)` is a partition. -/
def psumPart {n : ℕ} (μ : n.Partition) : MvPolynomial σ R :=
  (μ.parts.map (psum σ R)).prod

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