esymmPart_indiscrete

Mathlib.RingTheory.MvPolynomial.Symmetric.Defs

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

English

For the indiscrete partition, esymmPart equals esymm: esymmPart(Indiscrete n) = esymm(n).

Русский

При неизбирательном разложении esymmPart совпадает с esymm: esymmPart(Indiscrete n) = esymm(n).

LaTeX

$$$ esymmPart(\\sigma,R,\\mathrm{Indiscrete}(n)) = esymm(\\sigma,R,n) $$$

Lean4

@[simp]
theorem esymmPart_indiscrete (n : ℕ) : esymmPart σ R (.indiscrete n) = esymm σ R n := by cases n <;> simp [esymmPart]

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

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

Разделы

Аффилиация

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