instAddCommMonoidOreLocalization

Mathlib.RingTheory.OreLocalization.Basic

URI: https://scilib.ai/kg/mathlib#OreLocalization.instAddCommMonoidOreLocalization

English

The additive monoid structure is commutative on X[S⁻¹].

Русский

Аддитивная моноида на X[S⁻¹] является коммутативной.

LaTeX

$$AddCommMonoid (X[S^{-1}])$$

Lean4

instance instAddCommMonoidOreLocalization : AddCommMonoid X[S⁻¹] where add_comm := OreLocalization.add_comm

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

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

Разделы

Аффилиация

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