psum_zero

Mathlib.RingTheory.MvPolynomial.Symmetric.Defs

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

English

The degree-0 power sum equals the number of variables: psum(σ,R,0) = |σ|.

Русский

Степенная сумма нулевой степени равна числу переменных: psum(σ,R,0) = |σ|.

LaTeX

$$$\\mathrm{psum}_{\\sigma,R}(0) = |\\sigma|$$$

Lean4

@[simp]
theorem psum_zero : psum σ R 0 = Fintype.card σ := by simp [psum]

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

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

Разделы

Аффилиация

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