esymm_eq_multiset_esymm — Mathlib

English

The nth elementary symmetric polynomial in the variables X_i equals the nth elementary symmetric polynomial evaluated at the multiset {X_i | i ∈ univ}. In symbols, esymm(σR,n) = (univ.val.map X).esymm(n).

Русский

N-й элементарный симметрический полином по переменным X_i равен N-му элементарному симметрическому полиному, полученному от множества X_i интерпретированного как мульти множество: esymm(σ,R,n) = (univ.val.map X).esymm(n).

LaTeX

$$$ esymm(\\sigma,R,n) = (\\mathrm{univ}.val.map X)\\, .\\!\\text{esymm}\\\\(n). $$$

Lean4

/-- The `n`th elementary symmetric `MvPolynomial σ R` is obtained by evaluating the
`n`th elementary symmetric at the `Multiset` of the monomials -/
theorem esymm_eq_multiset_esymm : esymm σ R = (univ.val.map X).esymm := by
  exact funext fun n => (esymm_map_val X _ n).symm

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