hsymmPart

Mathlib.RingTheory.MvPolynomial.Symmetric.Defs

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

← MathLib Explorer

English

The 0-th hsymmPart is 1: hsymmPart(Indiscrete 0) = 1.

Русский

Нулевой части hsymmPart равна единице: hsymmPart(Indiscrete 0) = 1.

LaTeX

$$$ \\text{hsymmPart}(\\sigma,R,\\mathrm{Indiscrete}(0)) = 1 $$$

Lean4

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

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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