instLocalizationLocalizedModule — Mathlib

English

There is a canonical instance: if M is finite over R, then LocalizedModule S M is finite over Localization S.

Русский

Существует стандартный экземпляр: если M конечно над R, то LocalizedModule S M конечно над Localization S.

LaTeX

$$$\\text{Module.Finite} R\\ M \\Rightarrow \\text{Module.Finite} (\\mathrm{Localization}\\ S) (\\mathrm{LocalizedModule}\\ S\\ M)$$$

Lean4

instance [Module.Finite R M] : Module.Finite (Localization S) (LocalizedModule S M) :=
  of_isLocalizedModule S (LocalizedModule.mkLinearMap S M)

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