smul_mk — Mathlib

English

For r ∈ R and x ∈ M, r • Quotient.mk(I•⊤) x = Quotient.mk(I•⊤) (r • x).

Русский

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

LaTeX

$$smul_mk(I,r,x) : r • Quotient.mk(I•⊤) x = Quotient.mk(I•⊤) (r • x)$$

Lean4

theorem smul_mk {m n : ℕ} (hmn : m ≤ n) (r : AdicCauchySequence I R) (x : AdicCauchySequence I M) :
    r.val n • Submodule.Quotient.mk (p := (I ^ m • ⊤ : Submodule R M)) (x.val n) =
      r.val m • Submodule.Quotient.mk (p := (I ^ m • ⊤ : Submodule R M)) (x.val m) :=
  by
  rw [← Submodule.Quotient.mk_smul, ← Module.Quotient.mk_smul_mk, AdicCauchySequence.mk_eq_mk hmn, Ideal.mk_eq_mk I hmn,
    Module.Quotient.mk_smul_mk, Submodule.Quotient.mk_smul]

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