instModule

Mathlib.RingTheory.OreLocalization.Ring

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

English

Module structure on OreLocalization S X: OreLocalization S R acts on OreLocalization S X.

Русский

Модульная структура на OreLocalization S X: OreLocalization S R действует на OreLocalization S X.

LaTeX

$$Module (OreLocalization(S,R)) (OreLocalization(S,X))$$

Lean4

instance : Module R[S⁻¹] X[S⁻¹] where
  add_smul := OreLocalization.add_smul
  zero_smul := OreLocalization.zero_smul

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

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

Разделы

Аффилиация

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