msymm_isSymmetric

Mathlib.RingTheory.MvPolynomial.Symmetric.Defs

URI: https://scilib.ai/kg/mathlib#MvPolynomial.msymm_isSymmetric

English

For any μ, msymm σ R μ is a symmetric polynomial.

Русский

Для любого μ многочлен msymm(μ) симметричен.

LaTeX

$$$\\mathrm{msymm}_{\\sigma,R}(\\mu) \\text{ is symmetric}$$$

Lean4

theorem msymm_isSymmetric (μ : n.Partition) : IsSymmetric (msymm σ R μ) :=
  rename_msymm _ _ μ

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru