instQuotientIdealSpanSingletonSetSubmoduleHSMulTop

English

There is a quotient-ideal submodule hsmul top instantiation giving a quotient module structure.

Русский

Существуют экземпляры гомоморфизмов и подмодульов, образующие структуру квотиентного модуля.

LaTeX

$$Module(HasQuotient.Quotient R I) (HasQuotient.Quotient M (instHSMul.hSMul I Submodule.instTop.top))$$

Lean4

instance : Module (R ⧸ Ideal.span { r }) (M ⧸ r • (⊤ : Submodule R M)) :=
  (isTorsionBy_quotient_element_smul M r).module

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