esymm_pair_two

Mathlib.RingTheory.MvPolynomial.Symmetric.Defs

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

English

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

Русский

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

LaTeX

$$esymm (x ::ₘ { y }) 2 = x * y$$

Lean4

@[simp]
theorem esymm_pair_two (x y : R) : esymm (x ::ₘ { y }) 2 = x * y := by simp [esymm, powersetCard_one]

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

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

Разделы

Аффилиация

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