instQuotientIdealSubmoduleHSMulTop

English

There is a module structure on the quotient by span s for all r with IsTwoSided property.

Русский

Существует структура модуля на фактор-модуле по span s при двустороннем свойстве.

LaTeX

$$Module (HasQuotient.Quotient R (Ideal.span s)) (HasQuotient.Quotient M (span s Submodule.instTop.top))$$

Lean4

instance [I.IsTwoSided] : Module (R ⧸ I) (M ⧸ I • (⊤ : Submodule R M)) :=
  (isTorsionBySet_quotient_ideal_smul M I).module

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