instMonoid — Mathlib

English

The Ore localization carries a Monoid structure compatible with the localization operations.

Русский

Локализация Оре имеет структуру моноида, совместимую с операциями локализации.

LaTeX

$$$ (R[S^{-1}], \cdot) \text{ is a Monoid with } 1, \cdot \text{ defined by OreDiv, OreDivMulChar', etc.}$$$

Lean4

@[to_additive]
instance : Monoid R[S⁻¹] where
  one_mul := OreLocalization.one_mul
  mul_one := OreLocalization.mul_one
  mul_assoc := OreLocalization.mul_assoc
  npow := OreLocalization.npow

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