mk_smul_mk — Mathlib

English

There is a module instance for (R/I) acting on (M ⧸ I • ⊤) with I spanning.

Русский

Существует инстанс модуля для (R/I) на (M / (I • ⊤)).

LaTeX

$$Module (HasQuotient.Quotient R I) (HasQuotient.Quotient M (I.Submodule.Top))$$

Lean4

theorem mk_smul_mk [I.IsTwoSided] (r : R) (m : M) :
    Ideal.Quotient.mk I r • Submodule.Quotient.mk (p := (I • ⊤ : Submodule R M)) m =
      Submodule.Quotient.mk (p := (I • ⊤ : Submodule R M)) (r • m) :=
  rfl

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