psumPart_zero

Mathlib.RingTheory.MvPolynomial.Symmetric.Defs

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

English

For the indiscrete partition of 0, psumPart equals 1 (empty product).

Русский

Для indiscrete разложения 0 сумма psumPart равна единице (пустое произведение).

LaTeX

$$$\\mathrm{psumPart}_{\\sigma,R}(\\mathrm{Nat.Partition.indiscrete}(0)) = 1$$$

Lean4

@[simp]
theorem psumPart_zero : psumPart σ R (.indiscrete 0) = 1 := by simp [psumPart]

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

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

Разделы

Аффилиация

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