smul_mk — Mathlib

English

For any c in R and a ∈ M, the scalar action distributes: c • mk(a,b) = mk(c • a, b) in Localization(S).

Русский

Для любого c∈R и a∈M выполняется: c • mk(a,b) = mk(c • a, b) в Localization(S).

LaTeX

$$$c\\cdot \\big(\\mathrm{mk}(a,b)\\big) = \\mathrm{mk}(c\\cdot a, b).$$$

Lean4

theorem smul_mk [SMul R M] [IsScalarTower R M M] (c : R) (a b) : c • (mk a b : Localization S) = mk (c • a) b :=
  by
  rw [mk, mk, ← OreLocalization.smul_one_oreDiv_one_smul, OreLocalization.oreDiv_smul_oreDiv]
  change (c • 1) • a /ₒ (b * 1) = _
  rw [smul_assoc, one_smul, mul_one]
    -- move me

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