instMulActionOreLocalization — Mathlib

English

The Ore localization acts on the localized module X[S⁻¹] with unit and associative action.

Русский

Локализация Оре действует на локализованный модуль X[S⁻¹] с единичным и ассоциативным действием.

LaTeX

$$$ (R[S^{-1}]) \ acts\_on\ (X[S^{-1}]) \; with\; one\_smul,\; mul\_smul$$$

Lean4

@[to_additive]
instance instMulActionOreLocalization : MulAction R[S⁻¹] X[S⁻¹]
    where
  one_smul := OreLocalization.one_smul
  mul_smul := OreLocalization.mul_smul

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