addCommSemigroup

Mathlib.Algebra.Order.Positive.Ring

URI: https://scilib.ai/kg/mathlib#Positive.addCommSemigroup

← MathLib Explorer

English

Addition on the positive subtype is commutative: x+y = y+x for x,y > 0.

Русский

Сложение на подпределе положительных коммутативно: x+y = y+x.

LaTeX

$$$\\forall x,y>0:\\; x+y = y+x.$$$

Lean4

instance addCommSemigroup {M : Type*} [AddCommMonoid M] [Preorder M] [AddLeftStrictMono M] :
    AddCommSemigroup { x : M // 0 < x } :=
  fast_instance%Subtype.coe_injective.addCommSemigroup _ coe_add

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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