mk_smul_mk — Mathlib

English

For r ∈ R and x ∈ M, mk(I•⊤) r • mk x = r • mk x; i.e., scalar action commutes with quotient construction.

Русский

Для r и x: mk(I•⊤) r • mk x = r • mk x.

LaTeX

$$mk_smul_mk(I,r,x) : (Ideal.Quotient.mk (I•⊤) r) • (Submodule.Quotient.mk (p := (I•⊤)) x) = r • Submodule.Quotient.mk (p := (I•⊤)) x$$

Lean4

@[local simp]
theorem mk_smul_mk (r : R) (x : M) :
    Ideal.Quotient.mk (I • ⊤) r • Submodule.Quotient.mk (p := (I • ⊤ : Submodule R M)) x =
      r • Submodule.Quotient.mk (p := (I • ⊤ : Submodule R M)) x :=
  rfl

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