isModule' — Mathlib

English

There is a module structure on LocalizedModule S M over R, showing that LocalizedModule S M is a module compatible with the ambient ring R.

Русский

Существует структура модуля над R на LocalizedModule S M, что демонстрирует совместимость с окружающим кольцом R.

LaTeX

$$$\\text{LocalizedModule}(S,M)$ is a module over R$$

Lean4

noncomputable instance isModule' : Module R (LocalizedModule S M) :=
  { Module.compHom (LocalizedModule S M) <| algebraMap R (Localization S) with }

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