instIsLocalizedModuleQuotientSubmoduleLocalizedModuleLocalizationLocalizedToLocalizedQuotient

English

There is a canonical instance giving that Submodule.toLocalizedQuotient p M' is localized with respect to p and S.

Русский

Существует канонический экземпляр, доказывающий, что Submodule.toLocalizedQuotient p M′ локализуется при p и S.

LaTeX

$$$\mathrm{IsLocalizedModule}\ p\, (\mathrm{Submodule}.\mathrmtoLocalizedQuotient\; p\; M')$$$

Lean4

instance (M' : Submodule R M) : IsLocalizedModule p (M'.toLocalizedQuotient p) :=
  IsLocalizedModule.toLocalizedQuotient' _ _ _ _

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