psumPart_indiscrete

Mathlib.RingTheory.MvPolynomial.Symmetric.Defs

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

English

If n > 0, psumPart(μ) for the indiscrete partition μ = indiscrete(n) equals psum(σ,R,n).

Русский

Если n > 0, psumPart(μ) для indiscrete(n) равен psum(σ,R,n).

LaTeX

$$$\\mathrm{psumPart}_{\\sigma,R}(\\mathrm{Nat.Partition.indiscrete}(n)) = \\mathrm{psum}_{\\sigma,R}(n) \\quad (n \\neq 0)$$$

Lean4

@[simp]
theorem psumPart_indiscrete {n : ℕ} (npos : n ≠ 0) : psumPart σ R (.indiscrete n) = psum σ R n := by
  simp [psumPart, npos]

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

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

Разделы

Аффилиация

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