psum_one

Mathlib.RingTheory.MvPolynomial.Symmetric.Defs

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

English

The degree-1 power sum is the sum of the variables: psum(σ,R,1) = ∑ i X_i.

Русский

Степенная сумма первой степени равна сумме переменных: psum(σ,R,1) = ∑ i X_i.

LaTeX

$$$\\mathrm{psum}_{\\sigma,R}(1) = \\sum_{i \\in \\sigma} X_i$$$

Lean4

@[simp]
theorem psum_one : psum σ R 1 = ∑ i, X i := by simp [psum]

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

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

Разделы

Аффилиация

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