instAddGroupOreLocalization — Mathlib

English

Let R be a monoid, S a submonoid forming an Ore set, and X an AddGroup with a distributive action of R. Then the Ore localization X[S^{-1}] inherits a natural additive group structure.

Русский

Пусть R — моноид, S — подмоноид, образующий множество Ore, и X — аддитивная группа с распределимым действием R. Тогда локализация Ore X[S^{-1}] наследует естественную структуру аддитивной группы.

LaTeX

$$$\mathrm{AddGroup}\bigl(X[S^{-1}]\bigr)$$$

Lean4

instance instAddGroupOreLocalization : AddGroup X[S⁻¹]
    where
  neg_add_cancel := OreLocalization.neg_add_cancel
  zsmul := OreLocalization.zsmul

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