instDistribMulAction

Mathlib.RingTheory.OreLocalization.Basic

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

English

Ore localization carries a distributive multiplication action on X[S⁻¹].

Русский

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

LaTeX

$$DistribMulAction (OreLocalization S X)$$

Lean4

instance : DistribMulAction R[S⁻¹] X[S⁻¹]
    where
  smul_zero := OreLocalization.smul_zero
  smul_add := OreLocalization.smul_add

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

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

Разделы

Аффилиация

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