esymm_pair_one

Mathlib.RingTheory.MvPolynomial.Symmetric.Defs

URI: https://scilib.ai/kg/mathlib#Multiset.esymm_pair_one

English

For elements x,y in a commutative semiring R, esymm (x ::ₘ { y }) 1 equals x + y.

Русский

Для элементов x, y из коммутативного полупринятия R, esymm (x ::ₘ { y }) 1 равно x + y.

LaTeX

$$esymm (x ::ₘ { y }) 1 = x + y$$

Lean4

@[simp]
theorem esymm_pair_one (x y : R) : esymm (x ::ₘ { y }) 1 = x + y := by simp [esymm, powersetCard_one, add_comm]

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

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

Разделы

Аффилиация

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