esymmPart — Mathlib

English

For any partition μ = (μ1, μ2, ..., μr) of n, esymmPart(μ) equals the product of the elementary symmetric polynomials corresponding to each part: esymmPart(μ) = ∏_{j=1}^r esymm(μj).

Русский

Для разбиения μ = (μ1, μ2, ..., μr) числа n выражение esymmPart(μ) равно произведению соответствующих элементарных симметрических: esymmPart(μ) = ∏_{j=1}^r esymm(μj).

LaTeX

$$$\\text{Для частичной разбиения }\\mu=(\\mu_1,...,\\mu_r)\\text{ из }n:\\; \\text{esymmPart}(\\mu)=\\prod_{j=1}^r \\text{esymm}(\\mu_j).$$$

Lean4

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

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